diff options
| -rw-r--r-- | test-suite/success/Conjecture.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/test-suite/success/Conjecture.v b/test-suite/success/Conjecture.v index 93a4001a84..6db5859b37 100644 --- a/test-suite/success/Conjecture.v +++ b/test-suite/success/Conjecture.v @@ -1,6 +1,10 @@ -(* Test Conjecture/Admitted *) +(* 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. |