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/recdef.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/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9de15e407..ca0b9c5fe 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) = Anonymous)], GVar(d0,v_id)]) in - let body = fst (understand env Evd.empty glob_body)(*FIXME*) in + let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = @@ -1293,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in + let env = Global.env () in Proof_global.discard_all (); - build_proof Evd.empty + build_proof (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") @@ -1513,7 +1514,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let relation = fst (*FIXME*)(interp_constr env_with_pre_rec_args - Evd.empty + (Evd.from_env env_with_pre_rec_args) r) in let tcc_lemma_name = add_suffix function_name "_tcc" in |