From c22ac10752c12bcb23402ad29a73f2d9699248a6 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 26 Apr 2018 15:03:10 +0200 Subject: Deprecate Typing.e_* functions --- plugins/funind/functional_principles_proofs.ml | 3 ++- plugins/funind/functional_principles_types.ml | 6 ++++-- plugins/funind/indfun.ml | 3 ++- plugins/funind/invfun.ml | 6 ++++-- 4 files changed, 12 insertions(+), 6 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index a0616b308..44fa0740d 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1051,7 +1051,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in evd:=evd'; - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in + evd := sigma; res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 04a23cdb9..dc0f240bd 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in + evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -630,7 +631,8 @@ let build_scheme fas = in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in + evd := sigma; let c, u = try EConstr.destConst !evd f with DestKO -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7df57b577..efbd029e4 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -385,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in + let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in + evd := sigma; let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 28e85268a..094f54156 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info -- cgit v1.2.3