Skip to content

Commit 7cdc9c5

Browse files
committed
Don't require boolp in signed.v
1 parent b608eec commit 7cdc9c5

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

theories/signed.v

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
22
From Coq Require Import ssreflect ssrfun ssrbool.
33
From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint.
4-
Require Import boolp.
54

65
(******************************************************************************)
76
(* This file develops tools to make the manipulation of numbers with a known *)

0 commit comments

Comments
 (0)