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

diff --git a/test-suite/bugs/closed/1582.v b/test-suite/bugs/closed/1582.v
new file mode 100644
index 000000000..be5d3dd21
--- /dev/null
+++ b/test-suite/bugs/closed/1582.v
@@ -0,0 +1,15 @@
+Require Import Peano_dec.
+
+Definition fact_F :
+  forall (n:nat),
+  (forall m, m<n -> nat) ->
+  nat.
+refine
+  (fun n fact_rec =>
+     if eq_nat_dec n 0 then
+        1
+     else
+        let fn := fact_rec (n-1) _ in
+        n * fn).
+Admitted.
+