Imported Upstream version 8.4dfsgupstream/8.4dfsg

7 files changed, 55 insertions, 7 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bc..ee9e2504 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
     | t1,Leaf => t1
     | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1)
+          if (Z.eq_dec h2 1)
           then add v2 s
           else
             let (l2', r2') := split v1 u in
             join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1)
+          if (Z.eq_dec h1 1)
           then add v1 s
           else
             let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e86..fb2f0ca9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
     | I x =>
       match y with
-        | I y => if (Z_eq_dec x y) then in_left else in_right
+        | I y => if (Z.eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
     | S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f..17eeb352 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
 Require Import ZArith.
 
-Definition zeq := Z_eq_dec.
+Definition zeq := Z.eq_dec.
 
 Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
  fun y => if zeq x y then v else s y.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d49..d5837619 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
 
 Require Import ZArith.
 
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
 
 Lemma f_refl'' : forall n , f'' true n n.
 Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 0fc854b6..142ada26 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,8 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
    tactic but as a statically globalized one *)
 
 (* (this is a simplification of the original bug report) *)
 
 Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
 End A.
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v
new file mode 100644
index 00000000..08dff992
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2817.v
@@ -0,0 +1,9 @@
+(** Occur-check for Meta (up to application of already known instances) *)
+
+Goal forall (f: nat -> nat -> Prop) (x:bool)
+  (H: forall  (u: nat), f u u -> True)
+  (H0: forall x0, f (if x then x0 else x0) x0),
+False.
+
+intros.
+Fail apply H in H0. (* should fail without exhausting the stack *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v
new file mode 100644
index 00000000..a948b75e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2836.v
@@ -0,0 +1,39 @@
+(* Check that possible instantiation made during evar materialization
+   are taken into account and do not raise Not_found *)
+
+Set Implicit Arguments.
+
+Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
+  Object :> _ := obj;
+
+  Identity' : forall o, Morphism o o;
+  Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+}.
+
+Section SpecializedCategoryInterface.
+  Variable obj : Type.
+  Variable mor : obj -> obj -> Type.
+  Variable C : @SpecializedCategory obj mor.
+
+  Definition Morphism (s d : C) := mor s d.
+  Definition Identity (o : C) : Morphism o o := C.(Identity') o.
+  Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
+Morphism s d' := C.(Compose') s d d' m m0.
+End SpecializedCategoryInterface.
+
+Section ProductCategory.
+  Variable objC : Type.
+  Variable morC : objC -> objC -> Type.
+  Variable objD : Type.
+  Variable morD : objD -> objD -> Type.
+  Variable C : SpecializedCategory morC.
+  Variable D : SpecializedCategory morD.
+
+(* Should fail nicely *)
+Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
+=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
+Fail refine {|
+      Identity' := (fun o => (Identity (fst o), Identity (snd o)));
+      Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
+m2) (snd m1)))
+    |}.