From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 17:15:15 +0100 Subject: Removing compatibility layers in Retyping --- plugins/cc/cctac.ml | 4 ---- plugins/extraction/extraction.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 1 + plugins/funind/glob_term_to_relation.ml | 1 + plugins/funind/indfun.ml | 1 + plugins/funind/invfun.ml | 2 ++ plugins/micromega/coq_micromega.ml | 2 +- plugins/setoid_ring/newring.ml | 14 ++++++-------- plugins/ssrmatching/ssrmatching.ml4 | 7 ++++--- 9 files changed, 17 insertions(+), 17 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 7a99c45a8..a4ed4798a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -264,7 +264,6 @@ let refresh_universes ty k = let env = Proofview.Goal.env gl in let evm = Tacmach.New.project gl in let evm, ty = refresh_type env evm ty in - let ty = EConstr.of_constr ty in Sigma.Unsafe.of_pair (k ty, evm) end } @@ -387,7 +386,6 @@ let discriminate_tac (cstr,u as cstru) p = let trivial = EConstr.of_constr trivial in let evm = Tacmach.New.project gl in let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in - let intype = EConstr.of_constr intype in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in let pred = mkLambda(Name xid,outtype,mkRel 1) in @@ -496,9 +494,7 @@ let mk_eq f c1 c2 k = Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in let evm, ty = pf_apply type_of gl c1 in - let ty = EConstr.of_constr ty in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in - let ty = EConstr.of_constr ty in let term = mkApp (fc, [| ty; c1; c2 |]) in let evm, _ = type_of (pf_env gl) evm term in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 61547f96d..7b7e746f2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,7 +42,7 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) let sort_of env c = let polyprop = (lang() == Haskell) in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cc29d68f5..c98cdc467 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -985,6 +985,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in + let t = EConstr.Unsafe.to_constr t in decompose_prod_n_assum (nb_params + nb_args) t,evd in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 38cd21684..0725bb11c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1273,6 +1273,7 @@ let do_build_inductive Array.fold_right2 (fun id c (evd,env) -> let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in + let t = EConstr.Unsafe.to_constr t in evd, Environ.push_named (LocalAssum (id,t)) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 37a76bec1..1b899c152 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -373,6 +373,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error 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 (EConstr.of_constr uprinc) in + let princ_type = EConstr.Unsafe.to_constr princ_type in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca066c4cc..27528c2dc 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -135,6 +135,7 @@ let generate_type evd g_to_f f graph i = in evd:=evd'; let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in + let graph_arity = EConstr.Unsafe.to_constr graph_arity in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -203,6 +204,7 @@ let find_induction_principle evd f = | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in + let typ = EConstr.Unsafe.to_constr typ in evd:=evd'; rect_lemma,typ diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f96b189c5..ced572466 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -898,7 +898,7 @@ struct let has_typ gl t1 typ = let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in - Constr.equal ty typ + EConstr.eq_constr (Tacmach.project gl) ty (EConstr.of_constr typ) let is_convertible gl t1 t2 = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 131ecad33..c0eeff8d7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -344,6 +344,8 @@ let _ = add_map "ring" (****************************************************************************) (* Ring database *) +let pr_constr c = pr_constr (EConstr.Unsafe.to_constr c) + module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" @@ -357,12 +359,12 @@ let find_ring_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then + if not (Reductionops.is_conv env sigma ty ty') then user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; - (try ring_for_carrier ty + (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ @@ -495,7 +497,6 @@ let op_smorph r add mul req m1 m2 = (* (setoid,op_morph) *) let ring_equality env evd (r,add,mul,opp,req) = - let pr_constr c = pr_constr (EConstr.to_constr !evd c) in match EConstr.kind !evd req with | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) -> let setoid = plapp evd coq_eq_setoid [|r|] in @@ -553,7 +554,6 @@ let build_setoid_params env evd r add mul opp req eqth = let dest_ring env sigma th_spec = let th_typ = Retyping.get_type_of env sigma th_spec in - let th_typ = EConstr.of_constr th_typ in match EConstr.kind sigma th_typ with App(f,[|r;zero;one;add;mul;sub;opp;req|]) when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) -> @@ -585,7 +585,6 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in - let t = EConstr.of_constr t in plapp evd coq_mkhypo [|t;c|] let make_hyp_list env evd lH = @@ -820,7 +819,6 @@ let sf_sr = my_reference"SF_SR" let dest_field env evd th_spec = let open Termops in let th_typ = Retyping.get_type_of env !evd th_spec in - let th_typ = EConstr.of_constr th_typ in match EConstr.kind !evd th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) when is_global !evd (Lazy.force afield_theory) f -> @@ -852,12 +850,12 @@ let find_field_structure env sigma l = let ty = Retyping.get_type_of env sigma t in let check c = let ty' = Retyping.get_type_of env sigma c in - if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then + if not (Reductionops.is_conv env sigma ty ty') then user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; - (try field_for_carrier ty + (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> user_err ~hdr:"field" (str"cannot find a declared field structure over"++ diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d34c9325e..9798fa11c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1390,9 +1390,10 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let concl0 = pf_concl gl in let (t, uc), concl_x = fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in - let gl, tty = pf_type_of gl (EConstr.of_constr t) in - let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in - let concl = EConstr.of_constr concl in + let t = EConstr.of_constr t in + let concl_x = EConstr.of_constr concl_x in + let gl, tty = pf_type_of gl t in + let concl = EConstr.mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) -- cgit v1.2.3