From 98814890466b2ee4b72235a2591ecd150bff08e7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 May 2018 21:38:08 +0200
Subject: Fix #7586: Anomaly "Uncaught exception Not_found".

The old unification engine was using the unfiltered environment when a
context had been cleared, leading to an ill-typed goal.
---
 pretyping/unification.ml      | 2 +-
 test-suite/bugs/closed/7392.v | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/7392.v

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 62bee5a362..b9678fa106 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1391,7 +1391,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
 	      
   and mimick_undefined_evar evd flags hdc nargs sp =
     let ev = Evd.find_undefined evd sp in
-    let sp_env = Global.env_of_context ev.evar_hyps in
+    let sp_env = Global.env_of_context (evar_filtered_hyps ev) in
     let (evd', c) = applyHead sp_env evd nargs hdc in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
diff --git a/test-suite/bugs/closed/7392.v b/test-suite/bugs/closed/7392.v
new file mode 100644
index 0000000000..cf465c6588
--- /dev/null
+++ b/test-suite/bugs/closed/7392.v
@@ -0,0 +1,9 @@
+Inductive R : nat -> Prop := ER : forall n, R n -> R (S n).
+
+Goal (forall (n : nat), R n -> False) -> True -> False.
+Proof.
+intros H0 H1.
+eapply H0.
+clear H1.
+apply ER.
+simpl.
-- 
cgit v1.2.3