diff options
| -rw-r--r-- | test-suite/output/Sum.v | 3 | ||||
| -rw-r--r-- | test-suite/success/DHyp.v | 12 | ||||
| -rw-r--r-- | test-suite/success/Destruct.v | 9 | ||||
| -rw-r--r-- | test-suite/success/Print.v | 20 |
4 files changed, 44 insertions, 0 deletions
diff --git a/test-suite/output/Sum.v b/test-suite/output/Sum.v new file mode 100644 index 0000000000..aceadd121f --- /dev/null +++ b/test-suite/output/Sum.v @@ -0,0 +1,3 @@ +Check nat+nat+{True}. +Check {True}+{True}+{True}. +Check nat+{True}+{True}. diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v new file mode 100644 index 0000000000..330c21f01e --- /dev/null +++ b/test-suite/success/DHyp.v @@ -0,0 +1,12 @@ +HintDestruct Hypothesis a (le O ?) 3 (Inversion H). + +Goal ~(le O (S O)). +Intro H. +DHyp H. +Qed. + +HintDestruct Conclusion a (le O ?) 3 Constructor. + +Goal (le O O). +DConcl. +Qed. diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v new file mode 100644 index 0000000000..10df087289 --- /dev/null +++ b/test-suite/success/Destruct.v @@ -0,0 +1,9 @@ +(* Submitted by Robert Schneck *) + +Parameter A,B,C,D : Prop. +Axiom X : A->B->C/\D. + +Lemma foo : A->B->C. +Proof. +Intros. +NewDestruct X. (* Should find axiom X and should handle arguments of X *) diff --git a/test-suite/success/Print.v b/test-suite/success/Print.v new file mode 100644 index 0000000000..4554a84305 --- /dev/null +++ b/test-suite/success/Print.v @@ -0,0 +1,20 @@ +Print Tables. +Print ML Path. +Print ML Modules. +Print LoadPath. +Print Graph. +Print Coercions. +Print Classes. +Print nat. +Print Proof O. +Print All. +Print Grammar constr constr. +Inspect 10. + +Section A. +Coercion f := [x]True : nat -> Prop. +Print Coercion Paths nat SORTCLASS. + +Print Section A. +Print. + |