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, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2613.v b/test-suite/bugs/closed/2613.v
new file mode 100644
index 000000000..4f0470b1d
--- /dev/null
+++ b/test-suite/bugs/closed/2613.v
@@ -0,0 +1,17 @@
+(* Check that eq_sym is still pointing to Logic.eq_sym after use of Function *)
+
+Require Import ZArith.
+Require Recdef.
+
+Axiom nat_eq_dec: forall x y : nat, {x=y}+{x<>y}.
+
+Locate eq_sym.  (* Constant Coq.Init.Logic.eq_sym  *)
+
+Function loop (n: nat) {measure (fun x => x) n} : bool :=
+  if nat_eq_dec n 0 then false else loop (pred n).
+Proof.
+   admit.
+Defined.
+
+Check eq_sym eq_refl : 0=0.
+