Backporting from v8.2 to trunk:

- Filtering of doc compilation messages (11793,11795,11796).
- Fixing bug #1925 and cleaning around bug #1894 (11796, 11801).
- Adding some tests.



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

3 files changed, 38 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v
new file mode 100644
index 000000000..55fc82319
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1907.v
@@ -0,0 +1,7 @@
+(* An example of type inference *)
+
+Axiom A : Type.
+Definition f (x y : A) := x.
+Axiom g : forall x y : A, f x y = y -> Prop.
+Axiom x : A.
+Check (g x _ (refl_equal x)).
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
new file mode 100644
index 000000000..17eb721ad
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/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).
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v
new file mode 100644
index 000000000..7d9f9eb26
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1944.v
@@ -0,0 +1,9 @@
+(* Test some uses of ? in introduction patterns *)
+
+Inductive J : nat -> Prop := 
+  | K : forall p, J p -> (True /\ True)  -> J (S p).
+
+Lemma bug : forall n, J n -> J (S n).
+Proof.
+  intros ? H.
+  induction H as [? ? [? ?]].