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/1925.v b/test-suite/bugs/closed/1925.v
new file mode 100644
index 000000000..4caee1c36
--- /dev/null
+++ b/test-suite/bugs/closed/1925.v
@@ -0,0 +1,22 @@
+(* Check that the analysis of projectable rel's in an evar instance is up to
+   aliases *)
+
+Require Import List.
+
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C :=
+  fun x : A => g(f x).
+
+Definition map_fuse' :
+  forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A),
+    (map g (map f xs)) = map (compose _ _ _ g f) xs
+    :=
+    fun A B C g f =>
+      (fix loop (ys : list A) {struct ys} :=
+        match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
+        with
+        | nil => refl_equal nil
+        | x :: xs =>
+           match loop xs in eq _ a return eq _  ((g (f x)) :: a) with
+            | refl_equal => refl_equal (map g (map f (x :: xs)))
+           end
+        end).