summaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e51f5e0e..e4bde925 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 7113 2005-06-05 17:13:06Z barras $ *)
+(* $Id: unification.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
open Pp
open Util
@@ -259,7 +259,7 @@ let w_merge env with_types mod_delta metas evars evd =
end
and mimick_evar evd mod_delta hdc nargs sp =
- let ev = Evd.map (evars_of evd) sp in
+ let ev = Evd.find (evars_of evd) sp in
let sp_env = Global.env_of_context ev.evar_hyps in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (mc,ec) =