1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/Conjecture.v b/test-suite/success/Conjecture.v
new file mode 100644
index 00000000..6db5859b
--- /dev/null
+++ b/test-suite/success/Conjecture.v
@@ -0,0 +1,13 @@
+(* Check keywords Conjecture and Admitted are recognized *)
+
+Conjecture c : (n:nat)n=O.
+
+Check c.
+
+Theorem d : (n:nat)n=O.
+Proof.
+  NewInduction n.
+  Reflexivity.
+  Assert H:False.
+  2:NewDestruct H.
+Admitted.