summaryrefslogtreecommitdiff
path: root/proofs/evar_refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r--proofs/evar_refiner.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 4ee8001c..7a23d052 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
+(* $Id: evar_refiner.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
open Util
open Names
@@ -25,7 +25,7 @@ open Refiner
let w_refine env ev rawc evd =
if Evd.is_defined (evars_of evd) ev then
error "Instantiate called on already-defined evar";
- let e_info = Evd.map (evars_of evd) ev in
+ let e_info = Evd.find (evars_of evd) ev in
let env = Evd.evar_env e_info in
let sigma,typed_c =
Pretyping.Default.understand_tcc (evars_of evd) env