Fixing bug #4216:

Internal error: Anomaly: Uncaught exception Not_found. Please report.

An evarmap was lost because of an unsound typing primitive.

1 files changed, 4 insertions, 4 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fb7237e4b..ea74dc37e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -165,10 +165,10 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   in List.map try_occ occs
 
 let instantiate_lemma gl c ty l l2r concl =
-  let ct = pf_unsafe_type_of gl c in
-  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
-  let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
-   [eqclause]
+  let sigma, ct = pf_type_of gl c in
+  let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in
+  let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in
+  [eqclause]
 
 let rewrite_conv_closed_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;