summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2969.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/2969.v')
-rw-r--r--test-suite/bugs/closed/2969.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2969.v b/test-suite/bugs/closed/2969.v
index a03adbd7..7b1a2617 100644
--- a/test-suite/bugs/closed/2969.v
+++ b/test-suite/bugs/closed/2969.v
@@ -12,6 +12,7 @@ eexists.
reflexivity.
Grab Existential Variables.
admit.
+Admitted.
(* Alternative variant which failed but without raising anomaly *)
@@ -24,3 +25,4 @@ clearbody n n0.
exact I.
Grab Existential Variables.
admit.
+Admitted.