diff options
Diffstat (limited to 'src/PropToBool.v')
-rw-r--r-- | src/PropToBool.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/PropToBool.v b/src/PropToBool.v index 3d4dee3..bbcff4a 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -26,7 +26,11 @@ Ltac prop2bool := match goal with | [ |- forall _ : ?t, _ ] => lazymatch type of t with - | Prop => fail + | Prop => + match t with + | forall _ : _, _ => intro + | _ => fail + end | _ => intro end @@ -197,7 +201,7 @@ Ltac prop2bool_hyp H := [ bool2prop; apply H | ]; (* Replace the Prop version with the bool version *) - clear H; assert (H:=H'); clear H' + try clear H; let H := fresh H in assert (H:=H'); clear H' ]. Ltac prop2bool_hyps Hs := @@ -220,11 +224,14 @@ Section Test. prop2bool_hyp basic. prop2bool_hyp no_eq. prop2bool_hyp uninterpreted_type. + admit. + prop2bool_hyp plus_n_O. Abort. Goal True. Proof. - prop2bool_hyps (basic, no_eq, uninterpreted_type). + prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, plus_O_n). + admit. Abort. End Test. |