From e46ce40cee2c34f47acb55d2b24bd09f00987556 Mon Sep 17 00:00:00 2001
From: xclerc
Date: Fri, 20 Sep 2013 12:40:28 +0000
Subject: 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
---
 test-suite/bugs/closed/2001.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 test-suite/bugs/closed/2001.v

(limited to 'test-suite/bugs/closed/2001.v')

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.
-- 
cgit v1.2.3