From 775a02fa0d8df3eebf8a4f39a141504008a9a09a Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 21 Apr 2021 10:07:27 +0200 Subject: Port to 8.11 --- src/PropToBool.v | 4 ++-- 1 file 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. -- cgit