EConstr iterators respect the binding structure of cases.

Fixes #3166.

1 files changed, 0 insertions, 84 deletions

diff --git a/test-suite/bugs/opened/bug_3166.v b/test-suite/bugs/opened/bug_3166.v
deleted file mode 100644
index baf87631f0..0000000000
--- a/test-suite/bugs/opened/bug_3166.v
+++ /dev/null
@@ -1,84 +0,0 @@
-Set Asymmetric Patterns.
-
-Section eq.
-  Let A := { X : Type & X }.
-  Let B := (fun x : A => projT1 x).
-  Let T := (fun (a' : A) (b' : B a') => projT2 a' = b').
-  Let T' := T.
-  Let t1T := (fun _ : A => unit).
-  Let f1 := (fun x (_ : t1T x) => projT2 x).
-  Let t1 := (fun x (y : t1T x) => @eq_refl (projT1 x) (projT2 x)).
-  Let t1T' := t1T.
-  Let f1' := f1.
-  Let t1' := t1.
-
-  Theorem eq_matches_commute
-          a' b' (t' : T a' b')
-          (rta : forall b'', T' a' b'' -> A)
-          (rtb : forall b'' t'', B (rta b'' t''))
-          (rt1 : forall y, T _ (rtb (f1' a' y) (@t1' a' y)))
-          (R : forall (b : B (rta b' t')), T _ b -> Type)
-          (r1 : forall y, R (f1 _ y) (@t1 _ y))
-  : match
-      match t' as t0' in (@eq _ _ b0') return T (rta b0' t0') (rtb b0' t0') with
-        | eq_refl => rt1 tt
-      end
-      as t0 in (@eq _ _ b0)
-      return R b0 t0
-    with
-      | eq_refl => r1 tt
-    end
-    =
-    match t'
-          as t0' in (@eq _ _ b0')
-          return (forall (R : forall (b : B (rta b0' t0')), T _ b -> Type)
-                         (r1 : forall y, R (f1 _ y) (@t1 _ y)),
-                    R _ (match t0' as t0'0 in (@eq _ _ b0'0) return T (rta b0'0 t0'0) (rtb b0'0 t0'0) with
-                           | eq_refl => rt1 tt
-                         end))
-    with
-      | eq_refl => fun _ r1 =>
-                      match rt1 tt with
-                        | eq_refl => r1 tt
-                      end
-    end R r1.
-  Proof.
-    destruct t'; reflexivity.
-  Defined.
-
-  Theorem eq_match_beta2
-          a b (t : T a b)
-          X
-          (R : forall b' (t' : T a b'), X b' -> Type)
-          (r1 : forall y x, R _ (@t1 _ y) x)
-          x
-  : match t as t' in (@eq _ _ b') return forall x, R b' t' x with
-      | eq_refl => r1 tt
-    end (x b)
-    =
-    match t as t' in (@eq _ _ b') return R b' t' (x b') with
-      | eq_refl => r1 tt (x _)
-    end.
-  Proof.
-    destruct t; reflexivity.
-  Defined.
-End eq.
-
-Definition typeof {T} (_ : T) := T.
-
-Eval compute in (eq_sym (eq_sym _)).
-Goal forall T (x y : T) (p : x = y), True.
-  intros.
-  pose proof
-       (@eq_matches_commute
-          (existT (fun T => T) T x) y p
-          (fun b'' _ => existT (fun T => T) T b'')
-          (fun _ _ => x)
-          (fun _ => eq_refl)
-          (fun x' _ => x' = y)
-          (fun _ => eq_refl)
-        ) as H0.
-  compute in H0.
-  change (fun (x' : T) (_ : y = x') => x' = y) with ((fun y => fun (x' : T) (_ : y = x') => x' = y) y) in H0.
-  Fail pose proof (fun k => @eq_trans _ _ _ k H0).
-Abort.