From 836b9faa8797a2802c189e782469f8d2e467d894 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:15:05 +0200 Subject: Univs: fix evar_map leaks bugs in Function The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/g_indfun.ml4') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61f03d6f2..bc7e6f8b0 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -388,7 +388,7 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) | Some id -> let idref = const_of_id id in (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *) - let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in + let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in (fun u -> constr_head_match u idconstr) (* select only id *) | None -> (fun u -> isApp u) in (* select calls to any function *) let info_list = find_fapp test g in -- cgit v1.2.3