From d91addb140ba7315d70c4599b0d058bef798ac1c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2015 23:38:55 +0200
Subject: Fixing bug #4216:

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

An evarmap was lost because of an unsound typing primitive.
---
 tactics/equality.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fb7237e4b2..ea74dc37ea 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;
-- 
cgit v1.2.3