diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:15:05 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | 836b9faa8797a2802c189e782469f8d2e467d894 (patch) | |
| tree | 726906d8cf8e6c2da302a473514ff98af70faa56 /plugins/funind/g_indfun.ml4 | |
| parent | 72c6588923dca52be7bc7d750d969ff1baa76c45 (diff) | |
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.
Diffstat (limited to 'plugins/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |