*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2726 85f007b7-540e-0410-9357-904b9bb8a0f7

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.
+