diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-05-04 10:56:33 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-05-04 10:56:33 +0200 |
commit | f336abf5eae6eb0f664e2af4940df18fb47cc35f (patch) | |
tree | 308436c9b006d78a55d61c924fdc80e3cfa27a0b | |
parent | 1f21e1f95d43f5e76e38e1737de9a2a0322fd71c (diff) | |
parent | 677d88d7d3c48a43a45526ed72000d9c8c8a6e8b (diff) | |
download | smtcoq-f336abf5eae6eb0f664e2af4940df18fb47cc35f.tar.gz smtcoq-f336abf5eae6eb0f664e2af4940df18fb47cc35f.zip |
Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12
-rw-r--r-- | src/PropToBool.v | 48 |
1 files changed, 24 insertions, 24 deletions
diff --git a/src/PropToBool.v b/src/PropToBool.v index 5a7bf53..fcfe671 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -240,30 +240,30 @@ Ltac prop2bool_hyps Hs := -Section Test. - Variable A : Type. - - 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. - - Goal True. - Proof. - prop2bool_hyp basic. - prop2bool_hyp no_eq. - prop2bool_hyp uninterpreted_type. - admit. - prop2bool_hyp bool_eq. - prop2bool_hyp plus_n_O. - Abort. - - Goal True. - Proof. - prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n). - admit. - Abort. -End Test. +(* Section Test. *) +(* Variable A : Type. *) + +(* 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. *) + +(* Goal True. *) +(* Proof. *) +(* prop2bool_hyp basic. *) +(* prop2bool_hyp no_eq. *) +(* prop2bool_hyp uninterpreted_type. *) +(* admit. *) +(* prop2bool_hyp bool_eq. *) +(* prop2bool_hyp plus_n_O. *) +(* Abort. *) + +(* Goal True. *) +(* Proof. *) +(* prop2bool_hyps (basic, plus_n_O, no_eq, uninterpreted_type, bool_eq, plus_O_n). *) +(* admit. *) +(* Abort. *) +(* End Test. *) Section Group. |