1 files changed, 54 insertions, 4 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 0477377e..49bd77fc 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -71,13 +71,9 @@ Inductive Setoid : Type :=
 
 Definition elem (A : Setoid) := let (S, R, e) := A in S.
 
-(* <Warning> : Grammar is replaced by Notation *)
-
 Definition equal (A : Setoid) :=
   let (S, R, e) as s return (Relation (elem s)) := A in R.
 
-(* <Warning> : Grammar is replaced by Notation *)
-
 
 Axiom prf_equiv : forall A : Setoid, Equivalence (elem A) (equal A).
 Axiom prf_refl : forall A : Setoid, Reflexive (elem A) (equal A).
@@ -430,3 +426,57 @@ Definition f0 (F : False) (ty : bool) : bProp ty :=
   | _, false => F
   | _, true => I
   end.
+
+(* Simplification of bug/wish #1671 *)
+
+Inductive I : unit -> Type :=
+| C : forall a, I a -> I tt.
+
+(*
+Definition F (l:I tt) : l = l := 
+match l return l = l with
+| C tt (C _ l')  => refl_equal (C tt (C _ l'))
+end.
+
+one would expect that the compilation of F (this involves
+some kind of pattern-unification) would produce: 
+*)
+
+Definition F (l:I tt) : l = l := 
+match l return l = l with
+| C tt l' => match l' return C _ l' = C _ l' with C _ l''  => refl_equal (C tt (C _ l'')) end
+end.
+
+Inductive J : nat -> Type :=
+| D : forall a, J (S a) -> J a.
+
+(*
+Definition G (l:J O) : l = l := 
+match l return l = l with
+| D O (D 1 l')  => refl_equal (D O (D 1 l'))
+| D _ _  => refl_equal _
+end.
+
+one would expect that the compilation of G (this involves inversion)
+would produce:
+*)
+
+Definition G (l:J O) : l = l := 
+match l return l = l with
+| D 0 l'' =>
+    match l'' as _l'' in J n return
+      match n return forall l:J n, Prop with
+      | O => fun _ => l = l
+      | S p => fun l'' => D p l'' = D p l''
+      end _l'' with
+    | D 1 l'  => refl_equal (D O (D 1 l'))
+    | _ => refl_equal _
+    end
+| _ => refl_equal _
+end.
+
+Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) :=
+  match v with
+    | niln => w
+    | consn a n' v' => consn _ a _ (app v' w)
+  end.