diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:07:27 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-04-21 10:07:27 +0200 |
| commit | 775a02fa0d8df3eebf8a4f39a141504008a9a09a (patch) | |
| tree | 1ab49234eff1ffdb84d4c04113bfb15bd3c2bce0 | |
| parent | 5038242bff601d79d2fad04795fb7f1b77738291 (diff) | |
| download | smtcoq-775a02fa0d8df3eebf8a4f39a141504008a9a09a.tar.gz smtcoq-775a02fa0d8df3eebf8a4f39a141504008a9a09a.zip | |
Port to 8.11
| -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 3d4dee3..f4156b3 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -211,7 +211,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. @@ -281,7 +281,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. |