Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

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

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2001.v b/test-suite/bugs/closed/2001.v
new file mode 100644
index 0000000000..d0b3bf1732
--- /dev/null
+++ b/test-suite/bugs/closed/2001.v
@@ -0,0 +1,22 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+   computed when the user explicitly indicated it *)
+
+Unset Automatic Introduction.
+
+Inductive T : Set :=
+| v : T.
+
+Definition f (s:nat) (t:T) : nat.
+fix 2.
+intros s t.
+refine
+  match t with
+  | v => s
+  end.
+Defined.
+
+Lemma test :
+  forall s, f s v = s.
+Proof.
+reflexivity.
+Qed.