4 files changed, 43 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 0000000000..55fc823190
--- /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 0000000000..17eb721add
--- /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 0000000000..7d9f9eb267
--- /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 [? ? [? ?]].
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 4bdd579a60..d3b3689527 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -31,3 +31,8 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
 
 Notation "+1 x" := (S x) (at level 25, x at level 9).
 Section A. Global Notation "'Z'" := O (at level 9). End A.
+
+(* Check use of "$" (see bug #1961) *)
+
+Notation "$ x" := (id x) (at level 30).
+Check ($ 5).