Merge remote-tracking branch 'origin/coq-8.9' into coq-8.10

1 files changed, 24 insertions, 24 deletions

diff --git a/src/PropToBool.v b/src/PropToBool.v
index bdbfc8c..4b4f907 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.
-  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. *)
+(*   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.