Merge branch 'v8.5' into trunk

2 files changed, 51 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
index d00a707bd5..ae3e50d7ee 100644
--- a/test-suite/bugs/closed/HoTT_coq_014.v
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -122,6 +122,7 @@ Section GraphObj.
 
   Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
     GraphIndex_Morphism s d'.
+  Proof using.  (* This makes no sense, but it makes this test behave as before the no admit commit *)
   Admitted.
 
    Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
diff --git a/test-suite/success/tryif.v b/test-suite/success/tryif.v
new file mode 100644
index 0000000000..4394bddb3d
--- /dev/null
+++ b/test-suite/success/tryif.v
@@ -0,0 +1,50 @@
+Require Import TestSuite.admit.
+
+(** [not tac] is equivalent to [fail tac "succeeds"] if [tac] succeeds, and is equivalent to [idtac] if [tac] fails *)
+Tactic Notation "not" tactic3(tac) :=
+  (tryif tac then fail 0 tac "succeeds" else idtac); (* error if the tactic solved all goals *) [].
+
+(** Test if a tactic succeeds, but always roll-back the results *)
+Tactic Notation "test" tactic3(tac) := tryif not tac then fail 0 tac "fails" else idtac.
+
+Goal Set.
+Proof.
+  not fail.
+  not not idtac.
+  not fail 0.
+  (** Would be nice if we could get [not fail 1] to pass, maybe *)
+  not not admit.
+  not not test admit.
+  not progress test admit.
+  (* test grouping *)
+  not (not idtac; fail).
+  assert True.
+  all:not fail.
+  2:not fail.
+  all:admit.
+Defined.
+
+Goal Set.
+Proof.
+  test idtac.
+  test try fail.
+  test admit.
+  test match goal with |- Set => idtac end.
+  test (idtac; match goal with |- Set => idtac end).
+  (* test grouping *)
+  first [ (test idtac; fail); fail 1 | idtac ].
+  try test fail.
+  try test test fail.
+  test test idtac.
+  test test admit.
+  Fail test fail.
+  test (idtac; []).
+  test (assert True; [|]).
+  (* would be nice, perhaps, if we could catch [fail 1] and not just [fail 0] this *)
+  try ((test fail); fail 1).
+  assert True.
+  all:test idtac.
+  all:test admit.
+  2:test admit.
+  all:admit.
+Defined.