diff options
| author | Matthieu Sozeau | 2015-09-23 16:15:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | 836b9faa8797a2802c189e782469f8d2e467d894 (patch) | |
| tree | 726906d8cf8e6c2da302a473514ff98af70faa56 /plugins/funind/invfun.ml | |
| 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/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 89ceb751a4..d979401424 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs_constr = Array.map mkConstU funs in States.with_state_protection_on_exception (fun () -> - let evd = ref Evd.empty in + let env = Global.env () in + let evd = ref (Evd.from_env env) in let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i @@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( ) funs; - (* let evd = ref Evd.empty in *) let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> @@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) !evd + (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by |