diff options
Diffstat (limited to 'src/PropToBool.v')
| -rw-r--r-- | src/PropToBool.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/PropToBool.v b/src/PropToBool.v index bdbfc8c..d71c81c 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -243,7 +243,7 @@ Ltac prop2bool_hyps Hs := Section Test. Variable A : Type. - Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2. + Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat. Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z. Hypothesis uninterpreted_type : forall (a:A), a = a. Hypothesis bool_eq : forall (b:bool), negb (negb b) = b. @@ -318,7 +318,7 @@ End MultipleCompDec. polymorphism will be removed before *) Section Poly. Hypothesis basic : forall (A:Type) (l1 l2:list A), - length (l1++l2) = length l1 + length l2. + length (l1++l2) = (length l1 + length l2)%nat. Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a. Goal True. |