diff options
Diffstat (limited to 'src/PropToBool.v')
| -rw-r--r-- | src/PropToBool.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/PropToBool.v b/src/PropToBool.v index 4b4f907..fcfe671 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -164,10 +164,10 @@ Ltac prop2bool_hyp H := destruct HFalse | ]; clear H'; - match (eval compute in prop2bool_comp) with + lazymatch (eval compute in prop2bool_comp) with | true => let A := eval cbv in prop2bool_t in - match goal with + lazymatch goal with | [ _ : CompDec A |- _ ] => idtac | _ => let Hcompdec := fresh "Hcompdec" in @@ -195,7 +195,7 @@ Ltac prop2bool_hyp H := | _ => prop2bool end in tac_rec; - match goal with + lazymatch goal with | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g end; destruct HFalse @@ -213,9 +213,9 @@ Ltac prop2bool_hyp H := Ltac remove_compdec_hyp H := let TH := type of H in - match TH with + lazymatch TH with | forall p : CompDec ?A, _ => - match goal with + lazymatch goal with | [ p' : CompDec A |- _ ] => let H1 := fresh in assert (H1 := H p'); clear H; assert (H := H1); clear H1; @@ -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. |