Fix bug #5476: Ltac has an inconsistent view of hypotheses.

2 files changed, 30 insertions, 0 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 2eff1936f4..b16d044956 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -220,6 +220,8 @@ let instantiate_pattern env sigma lvar c =
               ctx
           in
 	  let c = substl inst c in
+	  (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *)
+	  let c = Evarutil.nf_evar sigma c in
 	  pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
 	with Not_found (* List.index failed *) ->
 	  let vars =
diff --git a/test-suite/bugs/closed/5476.v b/test-suite/bugs/closed/5476.v
new file mode 100644
index 0000000000..b2d9d943bc
--- /dev/null
+++ b/test-suite/bugs/closed/5476.v
@@ -0,0 +1,28 @@
+Require Setoid.
+
+Goal forall (P : Prop) (T : Type) (m m' : T) (T0 T1 : Type) (P2 : forall _ : 
+Prop, Prop) 
+            (P0 : Set) (x0 : P0) (P1 : forall (_ : P0) (_ : T), Prop)
+            (P3 : forall (_ : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (_ : 
+T) (_ : Prop), Prop)
+            (o : forall _ : P0, option T1)
+            (_ : P3
+                   (fun (k : P0) (_ : T0) (_ : Prop) =>
+                      match o k return Prop with
+                      | Some _ => True
+                      | None => False
+                      end) m' P) (_ : P2 (P1 x0 m))
+            (_ : forall (f : forall (_ : P0) (_ : T0) (_ : Prop), Prop) (m1 m2 
+: T) 
+                        (k : P0) (e : T0) (_ : P2 (P1 k m1)), iff (P3 f m2 P) 
+(f k e (P3 f m1 P))), False.
+Proof.
+  intros ???????????? H0 H H1.
+  rewrite H1 in H0; eauto with nocore.
+  { lazymatch goal with
+    | H : match ?X with _ => _ end |- _
+      => first [ lazymatch goal with
+                 | [ H' : context[X] |- _ ] => idtac H
+                 end
+               | fail 1 "could not find" X ]
+    end.