diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 17:47:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-13 19:11:10 +0200 |
| commit | 3a7095f9f6a09a4461c2124b0020dfe37962de26 (patch) | |
| tree | 02485f6b975a1c9b59f80fb8409ac5a614962a04 | |
| parent | 90d52ae25f08c5d1d58685e31073b8f3f37aad49 (diff) | |
Safer typing primitives.
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
44 files changed, 196 insertions, 163 deletions
@@ -20,6 +20,21 @@ Tactics * "Strict" changes the behavior of an unloaded hint to the one of the fail tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + + Changes from V8.5beta1 to V8.5beta2 =================================== diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 29bca8622..d5d6bdf74 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -513,7 +513,7 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_type_of state.gls trm in + let typ = pf_unsafe_type_of state.gls trm in let typ = canonize_name typ in let new_node= match t with @@ -836,7 +836,7 @@ let complete_one_class state i= let _,etyp,rest= destProd typ in let id = new_state_var etyp state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_type_of state.gls + let _c = pf_unsafe_type_of state.gls (constr_of_term (term state.uf pac.cnode)) in let _args = List.map (fun i -> constr_of_term (term state.uf i)) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 9952cb080..9c3a0f729 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -255,13 +255,13 @@ let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = Proofview.Goal.enter begin fun gl -> - let evm, _ = Tacmach.New.pf_apply e_type_of gl c in + let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) end let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of t = Tacmach.New.pf_type_of gl t in + let type_of t = Tacmach.New.pf_unsafe_type_of gl t in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> exact_check c @@ -331,7 +331,7 @@ let refute_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl in let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in @@ -341,14 +341,14 @@ let refute_tac c t1 t2 p = end let refine_exact_check c gl = - let evm, _ = pf_apply e_type_of gl c in + let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl in let neweq= new_app_global _eq [|sort;tt1;tt2|] in let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in @@ -373,7 +373,7 @@ let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl + Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl in let concl = Proofview.Goal.concl gl in (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) @@ -382,7 +382,7 @@ let discriminate_tac (cstr,u as cstru) p = (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_type_of gls identity in *) + (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in let outtype = mkSort outtype in @@ -486,7 +486,7 @@ let congruence_tac depth l = let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) let ty = (* Termops.refresh_universes *) (type_of c1) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 36273faae..714cd8634 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -773,7 +773,7 @@ let rec take_tac wits gls = match wits with [] -> tclIDTAC gls | wit::rest -> - let typ = pf_type_of gls wit in + let typ = pf_unsafe_type_of gls wit in tclTHEN (thus_tac wit typ []) (take_tac rest) gls @@ -854,7 +854,7 @@ let start_tree env ind rp = let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in let (ind,u) = @@ -869,7 +869,7 @@ let build_per_info etype casee gls = | _ -> mind.mind_nparams,None in let params,real_args = List.chop nparams args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let pred= List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in @@ -1228,13 +1228,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let nparams = mind.mind_nparams in let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5912f0a0c..c80a8081a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -105,7 +105,7 @@ let mk_open_instance id idc gl m t= let evmap=Refiner.project gl in let var_id= if id==dummy_id then dummy_bvid else - let typ=pf_type_of gl idc in + let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in @@ -154,7 +154,7 @@ let left_instance_tac (inst,id) continue seq= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in let evmap, _ = - try Typing.e_type_of (pf_env gl) evmap gt + try Typing.type_of (pf_env gl) evmap gt with e when Errors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (generalize [gt]) gl) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 802af04d0..96c4eb01e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl = let l = expand_constructor_hints l in let f gr (seq,gl) = let gl, c = pf_eapply Evd.fresh_global gl gr in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in (add_formula Hyp gr typ seq gl,gl) in List.fold_right f l (seq,gl) @@ -214,7 +214,7 @@ let extend_with_auto_hints l seq gl= | Res_pf_THEN_trivial_fail (c,_) -> (try let gr = global_of_constr c in - let typ=(pf_type_of gl c) in + let typ=(pf_unsafe_type_of gl c) in seqref:=add_formula Hint gr typ !seqref gl with Not_found->()) | _-> () in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4a832435f..169a70600 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -328,7 +328,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = let all_ids = pf_ids_of_hyps g in let new_ids,_ = list_chop ctxt_size all_ids in let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.e_type_of g to_refine in + let evm, _ = pf_apply Typing.type_of g to_refine in tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) in @@ -543,7 +543,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -593,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in (* compute the new value of the body *) let new_term_value = match kind_of_term new_term_value_eq with @@ -606,7 +606,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = in let fun_body = mkLambda(Anonymous, - pf_type_of g' term, + pf_unsafe_type_of g' term, Termops.replace_term term (mkRel 1) dyn_infos.info ) in @@ -638,7 +638,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in - let evm, _ = pf_apply Typing.e_type_of g c in + let evm, _ = pf_apply Typing.type_of g c in tclTHENLIST[ Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); @@ -699,7 +699,7 @@ let build_proof let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (pf_concl g) in - let type_of_term = pf_type_of g t in + let type_of_term = pf_unsafe_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -919,7 +919,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_type_of g (mkVar hyp) in + let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> if Id.List.mem hyp hyps @@ -964,7 +964,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = - let evd,t = Typing.e_type_of ~refresh:true (Global.env ()) evd f + let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f in decompose_prod_n_assum (nb_params + nb_args) t,evd @@ -1034,8 +1034,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' res in - evd:=evd'; + evd:=evd'; + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in let nb_intro_to_do = nb_prod (pf_concl g) in @@ -1414,7 +1414,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (pf_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in let f_app = Array.last (snd (destApp hrec_concl)) in let f = (fst (destApp f_app)) in let rec backtrack : tactic = @@ -1641,7 +1641,7 @@ let prove_principle_for_gen (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) (* observe_tac "h_fix " *) (fix (Some fix_id) (List.length args_ids + 1)); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_type_of g (mkVar fix_id) )); tclIDTAC g); *) +(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); (* observe_tac "finish" *) (fun gl' -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a2bbf97ae..3edc590cc 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -274,7 +274,7 @@ 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_________") [] in - let _ = evd := fst(Typing.e_type_of ~refresh:true (Global.env ()) !evd new_principle_type ) in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -327,7 +327,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let s = Universes.new_sort_in_family fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in - let evd' = fst (Typing.e_type_of ~refresh:true (Global.env ()) evd' value) in + let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in ignore( @@ -478,7 +478,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in let _ = evd := sigma in let l_schemes = - List.map (Typing.type_of env sigma) schemes + List.map (Typing.unsafe_type_of env sigma) schemes in let i = ref (-1) in let sorts = @@ -608,8 +608,8 @@ let build_scheme fas = (str "Cannot find " ++ Libnames.pr_reference f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in - let evd',_ = Typing.e_type_of ~refresh:true (Global.env ()) evd' f in - let _ = evd := evd' in + let _ = evd := evd' in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in (destConst f,sort) ) fas @@ -659,7 +659,7 @@ let build_case_scheme fa = in let sigma, scheme = (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in - let scheme_type = (Typing.type_of env sigma ) scheme in + let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 043d4328c..61f03d6f2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -321,7 +321,7 @@ let mkEq typ c1 c2 = let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_type_of gl cstr in + let typ = Tacmach.pf_unsafe_type_of gl cstr in tclTHEN (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)) (tclTHENFIRST @@ -349,7 +349,7 @@ let rec poseq_list_ids_rec lcstr gl = let _ = prstr "c = " in let _ = prconstr c in let _ = prstr "\n" in - let typ = Tacmach.pf_type_of gl c in + let typ = Tacmach.pf_unsafe_type_of gl c in let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in let x = Tactics.fresh_id [] cname gl in let _ = list_constr_largs:=mkVar x :: !list_constr_largs in @@ -478,8 +478,8 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF (CRef (Libnames.Ident (Loc.ghost,id1),None)) in let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty (CRef (Libnames.Ident (Loc.ghost,id2),None)) in - let f1type = Typing.type_of (Global.env()) Evd.empty f1 in - let f2type = Typing.type_of (Global.env()) Evd.empty f2 in + let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in + let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in let ar1 = List.length (fst (decompose_prod f1type)) in let ar2 = List.length (fst (decompose_prod f2type)) in let _ = diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9e3f39863..065c12a2d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -487,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in - let rt_typ = Typing.type_of env Evd.empty rt_as_constr in + let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -595,7 +595,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env Evd.empty v in - let v_type = Typing.type_of env Evd.empty v_as_constr in + let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr in let new_env = match n with Anonymous -> env @@ -611,7 +611,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -643,7 +643,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = nal in let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.type_of env Evd.empty b_as_constr in + let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr in let (ind,_) = try Inductiveops.find_inductive env Evd.empty b_typ with Not_found -> @@ -690,7 +690,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in - Typing.type_of env Evd.empty case_arg_as_constr + Typing.unsafe_type_of env Evd.empty case_arg_as_constr ) el in (****** The next works only if the match is not dependent ****) @@ -737,7 +737,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.type_of env_with_pat_ids Evd.empty (mkVar id) + Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] @@ -791,7 +791,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env Evd.empty (mkVar id) in let raw_typ_of_id = Detyping.detype false [] new_env Evd.empty typ_of_id in @@ -1105,7 +1105,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = begin let not_free_in_t id = not (is_free_in id t) in let t',ctx = Pretyping.understand env Evd.empty t in - let type_t' = Typing.type_of env Evd.empty t' in + let type_t' = Typing.unsafe_type_of env Evd.empty t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1255,7 +1255,7 @@ let do_build_inductive let evd,env = Array.fold_right2 (fun id c (evd,env) -> - let evd,t = Typing.e_type_of env evd (mkConstU c) in + let evd,t = Typing.type_of env evd (mkConstU c) in evd, Environ.push_named (id,None,t) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e211b6883..5dcb0c043 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -72,11 +72,11 @@ let functional_induction with_clean c princl pat = errorlabstrm "" (str "Cannot find induction principle for " ++Printer.pr_lconstr (mkConst c') ) in - (princ,NoBindings, Tacmach.pf_type_of g' princ,g') + (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g') | _ -> raise (UserError("",str "functional induction must be used with a function" )) end | Some ((princ,binding)) -> - princ,binding,Tacmach.pf_type_of g princ,g + princ,binding,Tacmach.pf_unsafe_type_of g princ,g in let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = @@ -356,8 +356,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (fun i x -> let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in - let evd',princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd' uprinc in - let _ = evd := evd' in + let _ = evd := evd' in + let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d10924f88..89ceb751a 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -127,8 +127,8 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph))) in - let evd',graph_arity = Typing.e_type_of (Global.env ()) evd' graph in evd:=evd'; + let graph_arity = Typing.e_type_of (Global.env ()) evd graph in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -193,7 +193,7 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let evd',typ = Typing.e_type_of ~refresh:true (Global.env ()) evd' rect_lemma in + let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -296,7 +296,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_type_of g (mkVar hid) in + let type_of_hid = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_hid with | Prod(_,_,t') -> begin @@ -440,7 +440,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes "functional_induction" ( (fun gl -> let term = mkApp (mkVar principle_id,Array.of_list bindings) in - let gl', _ty = pf_eapply (Typing.e_type_of ~refresh:true) gl term in + let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl term in Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) @@ -577,7 +577,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match kind_of_term (pf_type_of g (mkVar id)) with + match kind_of_term (pf_unsafe_type_of g (mkVar id)) with | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -642,7 +642,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in let graph_principle = nf_zeta schemes.(i) in - let princ_type = pf_type_of g graph_principle in + let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig princ_type in (* Then we get the number of argument of the function and compute a fresh name for each of them @@ -772,7 +772,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = evd := fst (Typing.e_type_of (Global.env ()) !evd type_of_lemma) in + let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in let type_of_lemma = nf_zeta type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info @@ -900,7 +900,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing *) let revert_graph kn post_tac hid g = - let typ = pf_type_of g (mkVar hid) in + let typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term typ with | App(i,args) when isInd i -> let ((kn',num) as ind'),u = destInd i in @@ -951,7 +951,7 @@ let revert_graph kn post_tac hid g = let functional_inversion kn hid fconst f_correct : tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in - let type_of_h = pf_type_of g (mkVar hid) in + let type_of_h = pf_unsafe_type_of g (mkVar hid) in match kind_of_term type_of_h with | App(eq,args) when eq_constr eq (make_eq ()) -> let pre_tac,f_args,res = @@ -1003,7 +1003,7 @@ let invfun qhyp f g = Proofview.V82.of_tactic begin Tactics.try_intros_until (fun hid -> Proofview.V82.tactic begin fun g -> - let hyp_typ = pf_type_of g (mkVar hid) in + let hyp_typ = pf_unsafe_type_of g (mkVar hid) in match kind_of_term hyp_typ with | App(eq,args) when eq_constr eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b9902a9fc..d3979748e 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,7 +115,7 @@ let pf_get_new_ids idl g = let compute_renamed_type gls c = rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] - (pf_type_of gls c) + (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -400,7 +400,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = thin to_intros; h_intros to_intros; (fun g' -> - let ty_teq = pf_type_of g' (mkVar heq) in + let ty_teq = pf_unsafe_type_of g' (mkVar heq) in let teq_lhs,teq_rhs = let _,args = try destApp ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -514,13 +514,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app (pf_type_of g (mkVar id)) with + match decompose_app (pf_unsafe_type_of g (mkVar id)) with | _, t::_ -> eq_constr t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (str "prove_lt") (prove_lt hyple) @@ -655,7 +655,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} let pf_type c tac gl = - let evars, ty = Typing.e_type_of (pf_env gl) (project gl) c in + let evars, ty = Typing.type_of (pf_env gl) (project gl) c in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl let pf_typel l tac = @@ -680,7 +680,7 @@ let mkDestructEq : if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in - let type_of_expr = pf_type_of g expr in + let type_of_expr = pf_unsafe_type_of g expr in let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4e2696dfd..710a2394d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1689,7 +1689,7 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.nf_enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 2f9e8509c..e590958cc 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -162,7 +162,7 @@ let ic_unsafe c = (*FIXME remove *) let env = Global.env() and sigma = Evd.empty in fst (Constrintern.interp_constr env sigma c) -let ty c = Typing.type_of (Global.env()) Evd.empty c +let ty c = Typing.unsafe_type_of (Global.env()) Evd.empty c let decl_constant na ctx c = let vars = Universes.universes_of_constr c in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fcbe90b6a..ef196e0a7 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1668,7 +1668,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.e_type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in @@ -2014,7 +2014,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env - {uj_val = ty; uj_type = Typing.type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} in let (ind,u), params = dest_ind_family indf in if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind; @@ -2214,7 +2214,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8ebb8cd27..f5135f5c6 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in (try subco () with NoSubtacCoercion -> - let typ = Typing.type_of env evm c in - let typ' = Typing.type_of env evm c' in + let typ = Typing.unsafe_type_of env evm c in + let typ' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') (* else subco () *) @@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in - let lam_type = Typing.type_of env evm c in - let lam_type' = Typing.type_of env evm c' in + let lam_type = Typing.unsafe_type_of env evm c in + let lam_type' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' (* ) else subco () *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0cadffa4f..03fe2122c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -374,7 +374,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.type_of env evd c in + let ty = Typing.unsafe_type_of env evd c in make_judge c ty let judge_of_Type evd s = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 372b26aa2..8a5db9059 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1134,7 +1134,7 @@ let abstract_scheme env (locc,a) (c, sigma) = let pattern_occs loccs_trm env sigma c = let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in try - let _ = Typing.type_of env sigma abstr_trm in + let _ = Typing.unsafe_type_of env sigma abstr_trm in sigma, applist(abstr_trm, List.map snd loccs_trm) with Type_errors.TypeError (env',t) -> raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t)))) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c6209cc33..fb5927dbf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -270,7 +270,7 @@ let check env evdref c t = (* Type of a constr *) -let type_of env evd c = +let unsafe_type_of env evd c = let j = execute env (ref evd) c in j.uj_type @@ -283,7 +283,7 @@ let sort_of env evdref c = (* Try to solve the existential variables by typing *) -let e_type_of ?(refresh=false) env evd c = +let type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) @@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type +let e_type_of ?(refresh=false) env evdref c = + let j = execute env evdref c in + (* side-effect on evdref *) + if refresh then + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let () = evdref := evd in + c + else j.uj_type + let solve_evars env evdref c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f822f1a5..bfae46ff8 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -13,12 +13,15 @@ open Evd (** This module provides the typing machine with existential variables and universes. *) -(** Typecheck a term and return its type *) -val type_of : env -> evar_map -> constr -> types +(** Typecheck a term and return its type. May trigger an evarmap leak. *) +val unsafe_type_of : env -> evar_map -> constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types + +(** Variant of [type_of] using references instead of state-passing. *) +val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) val sort_of : env -> evar_map ref -> types -> sorts diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c2281e13a..b5fe5d0b6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -93,7 +93,7 @@ let abstract_list_all env evd typ c l = let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in let evd,typp = - try Typing.e_type_of env evd p + try Typing.type_of env evd p with | UserError _ -> error_cannot_find_well_typed_abstraction env evd p l None @@ -1150,7 +1150,7 @@ let applyHead env evd n c = apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.type_of env evd c) evd + apprec n c (Typing.unsafe_type_of env evd c) evd let is_mimick_head ts f = match kind_of_term f with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2c9c695bf..a2cccc0e0 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -28,7 +28,7 @@ open Misctypes (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 898588d9e..5c48995fc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -83,7 +83,7 @@ let apply_to_hyp sign id f = else sign let check_typability env sigma c = - if !check then let _ = type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma c in () (************************************************************************) (************************************************************************) @@ -317,7 +317,7 @@ let meta_free_prefix a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then type_of env sigma c + if !check then unsafe_type_of env sigma c else Retyping.get_type_of env sigma c let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index fa0d03623..4238d1e37 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -84,6 +84,7 @@ let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of @@ -172,6 +173,9 @@ module New = struct let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl + let pf_unsafe_type_of gl t = + pf_apply unsafe_type_of gl t + let pf_type_of gl t = pf_apply type_of gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index f7fc6b54f..a0e1a0157 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,7 +41,8 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> named_declaration val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> constr -> types +val pf_type_of : goal sigma -> constr -> evar_map * types val pf_hnf_type_of : goal sigma -> constr -> types val pf_get_hyp : goal sigma -> Id.t -> named_declaration @@ -112,7 +113,8 @@ module New : sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_concl : [ `NF ] Proofview.Goal.t -> types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types + val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ad8164fa6..2b3fadf7f 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -263,7 +263,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = try let others,(c1,c2) = split_last_two args in let ty1, ty2 = - Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -281,7 +281,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = | None -> None let find_applied_relation metas loc env sigma c left2right = - let ctype = Typing.type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma c in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 6ea25269c..ef78a953a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -149,7 +149,7 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = clenv'.evd} else c, gl in - let t1 = pf_type_of gl c in + let t1 = pf_unsafe_type_of gl c in tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl let unify_e_resolve poly flags (c,clenv) gls = @@ -168,7 +168,7 @@ let unify_resolve poly flags (c,clenv) gls = let clenv_of_prods poly nprods (c, clenv) gls = if poly || Int.equal nprods 0 then Some clenv else - let ty = pf_type_of gls c in + let ty = pf_unsafe_type_of gls c in let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) @@ -842,6 +842,6 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_type_of gl c in + let cty = pf_unsafe_type_of gl c in let ce = mk_clenv_from gl (c,cty) in unify_e_resolve false flags (c,ce) gl diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c03710e91..22f218b4f 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -90,7 +90,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.nf_enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 50925ecde..34f87c6cf 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -33,7 +33,7 @@ DECLARE PLUGIN "eauto" let eauto_unif_flags = auto_flags_of_state full_transparent_state -let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in +let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_unsafe_type_of gl c) and t2 = pf_concl gl in if occur_existential t1 || occur_existential t2 then tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl else Proofview.V82.of_tactic (exact_check c) gl diff --git a/tactics/elim.ml b/tactics/elim.ml index 3cb4fa9c4..4841d2c25 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -85,7 +85,7 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) @@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.nf_enter begin fun gl -> - let idty = pf_type_of gl (mkVar id) in + let idty = pf_unsafe_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) idty in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 2ee4bf8e1..a5d68e19b 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -133,7 +133,7 @@ let match_eqdec c = let solveArg eqonleft op a1 a2 tac = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl a1 in + let rectype = pf_unsafe_type_of gl a1 in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let subtacs = if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] @@ -203,7 +203,7 @@ let decideEquality rectype = let compare c1 c2 = Proofview.Goal.enter begin fun gl -> - let rectype = pf_type_of gl c1 in + let rectype = pf_unsafe_type_of gl c1 in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro diff --git a/tactics/equality.ml b/tactics/equality.ml index 593b7e9ea..fb7237e4b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -165,7 +165,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let ct = pf_type_of gl c in + let ct = pf_unsafe_type_of gl c in let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in [eqclause] @@ -944,7 +944,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.nf_enter begin fun gl -> - let type_of = pf_type_of gl in + let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in @@ -1019,7 +1019,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in - let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in + let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in let (na,_,_) = lookup_rel lind env in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1053,7 +1053,7 @@ let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in let combined_rels = Int.Set.union prev_rels direct_rels in - let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (mkRel i))) in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) in minimalrec_free_rels_rec Int.Set.empty @@ -1099,7 +1099,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let rec sigrec_clausal_form siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) - let dflt_typ = type_of env sigma dflt in + let dflt_typ = unsafe_type_of env sigma dflt in try let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in @@ -1118,7 +1118,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (destEvar ev) with | Some w -> - let w_type = type_of env sigma w in + let w_type = unsafe_type_of env sigma w in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) @@ -1200,7 +1200,7 @@ let make_iterated_tuple env sigma dflt (z,zty) = sigma, (tuple,tuplety,dfltval) let rec build_injrec env sigma dflt c = function - | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma c) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1253,7 +1253,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in @@ -1293,7 +1293,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let injfun = mkNamedLambda e t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in - let sigma, pf_typ = Typing.e_type_of env sigma pf in + let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in let pf = Clenvtac.clenv_value_cast_meta inj_clause in let ty = simplify_args env sigma (clenv_type inj_clause) in @@ -1460,8 +1460,8 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Simulate now the normalisation treatment made by Logic.mk_refgoals *) let expected_goal = nf_betaiota sigma expected_goal in (* Retype to get universes right *) - let sigma, expected_goal_ty = Typing.e_type_of env sigma expected_goal in - let sigma, _ = Typing.e_type_of env sigma body in + let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in + let sigma, _ = Typing.type_of env sigma body in sigma,body,expected_goal (* Like "replace" but decompose dependent equalities *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index f217cda89..177be2c20 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -704,7 +704,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in Tacticals.New.tclTHENLIST [Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]); Proofview.Goal.nf_enter begin fun gl -> @@ -755,7 +755,7 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/tactics/hints.ml b/tactics/hints.ml index ae45aabd0..0df1a35c6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -780,7 +780,7 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (type_of env sigma c) in + let t = hnf_constr env sigma (unsafe_type_of env sigma c) in let hd = head_of_constr_reference (head_constr t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4b94f420b..95f3af57e 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -411,7 +411,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_type_of gl e1 in (t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl t1 t2 then (t1,e1,e2) diff --git a/tactics/inv.ml b/tactics/inv.ml index 5502356fb..ef115aea0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -123,13 +123,13 @@ let make_inv_predicate env evd indf realargs id status concl = let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in build_concl eqns args (succ n) restlist in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in - let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args @@ -437,7 +437,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in Errors.errorlabstrm "" msg diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index d48731773..6d26e91c6 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -381,7 +381,7 @@ end let type_app_poly env env evd f args = let evars, c = app_poly_nocheck env evd f args in - let evd', t = Typing.e_type_of env (goalevars evars) c in + let evd', t = Typing.type_of env (goalevars evars) c in (evd', cstrevars evars), c module PropGlobal = struct @@ -472,7 +472,7 @@ let rec decompose_app_rel env evd t = | App (f, [||]) -> assert false | App (f, [|arg|]) -> let (f', argl, argr) = decompose_app_rel env evd arg in - let ty = Typing.type_of env evd argl in + let ty = Typing.unsafe_type_of env evd argl in let f'' = mkLambda (Name default_dependent_ident, ty, mkLambda (Name (Id.of_string "y"), lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) @@ -747,7 +747,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let morphargs, morphobjs = Array.chop first args in let morphargs', morphobjs' = Array.chop first args' in let appm = mkApp(m, morphargs) in - let appmtype = Typing.type_of env (goalevars evars) appm in + let appmtype = Typing.unsafe_type_of env (goalevars evars) appm in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1738,7 +1738,7 @@ let declare_projection n instance_id r = let poly = Global.is_polymorphic r in let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in let term = proper_projection c ty in - let typ = Typing.type_of (Global.env ()) Evd.empty term in + let typ = Typing.unsafe_type_of (Global.env ()) Evd.empty term in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1771,7 +1771,7 @@ let build_morphism_signature m = let env = Global.env () in let m,ctx = Constrintern.interp_constr env Evd.empty m in let sigma = Evd.from_env ~ctx env in - let t = Typing.type_of env sigma m in + let t = Typing.unsafe_type_of env sigma m in let cstrs = let rec aux t = match kind_of_term t with @@ -1798,7 +1798,7 @@ let build_morphism_signature m = let default_morphism sign m = let env = Global.env () in - let t = Typing.type_of env Evd.empty m in + let t = Typing.unsafe_type_of env Evd.empty m in let evars, _, sign, cstrs = PropGlobal.build_signature (Evd.empty, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -1994,7 +1994,7 @@ let setoid_proof ty fn fallback = try let rel, _, _ = decompose_app_rel env sigma concl in let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in + let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in (try init_setoid () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e @@ -2053,7 +2053,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> - let ctype = pf_type_of gl (mkVar id) in + let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7ce158fd1..374c7c736 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -734,7 +734,7 @@ let interp_may_eval f ist env sigma = function str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in - Typing.e_type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma c_interp | ConstrTerm c -> try f ist env sigma c diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5ba53a764..7d1cc3341 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -598,7 +598,7 @@ module New = struct (** FIXME: evar leak. *) let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv @@ -651,7 +651,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3038a9506..2791d7c48 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -158,7 +158,7 @@ let convert_concl ?(check=true) ty k = Proofview.Refine.refine ~unsafe:true begin fun sigma -> let sigma = if check then begin - ignore (Typing.type_of env sigma ty); + ignore (Typing.unsafe_type_of env sigma ty); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; sigma @@ -628,7 +628,7 @@ let change_on_subterm cv_pb deep t where env sigma c = env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.type_of env sigma c) + try ignore (Typing.unsafe_type_of env sigma c) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; @@ -979,7 +979,7 @@ let cut c = let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) - let typ = Typing.type_of env sigma c in + let typ = Typing.unsafe_type_of env sigma c in let typ = whd_betadeltaiota env sigma typ in match kind_of_term typ with | Sort _ -> true @@ -1224,7 +1224,7 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_type_of gl c) in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1639,7 +1639,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter begin fun gl -> - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with + match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -1672,7 +1672,7 @@ let exact_check c = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, ct = Typing.e_type_of env sigma c in + let sigma, ct = Typing.type_of env sigma c in Proofview.Unsafe.tclEVARS sigma <*> Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end @@ -1821,7 +1821,7 @@ let specialize (c,lbind) g = let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in tclEVARS evd, nf_evar evd c else - let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in + let clause = pf_apply make_clenv_binding g (c,pf_unsafe_type_of g c) lbind in let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in @@ -1841,11 +1841,11 @@ let specialize (c,lbind) g = | Var id when Id.List.mem id (pf_ids_of_hyps g) -> tclTHEN tac (tclTHENFIRST - (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (assert_before_replacing id (pf_unsafe_type_of g term)) g) (exact_no_check term)) g | _ -> tclTHEN tac (tclTHENLAST - (fun g -> Proofview.V82.of_tactic (cut (pf_type_of g term)) g) + (fun g -> Proofview.V82.of_tactic (cut (pf_unsafe_type_of g term)) g) (exact_no_check term)) g (* Keeping only a few hypotheses *) @@ -1980,7 +1980,7 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -1994,7 +1994,7 @@ let intro_decomp_eq loc l thin tac id = let intro_or_and_pattern loc bracketed ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let nv = constructors_nrealargs ind in let ll = fix_empty_or_and_pattern (Array.length nv) ll in @@ -2013,7 +2013,7 @@ let rewrite_hyp assert_style l2r id = let clear_var_and_eq c = tclTHEN (clear [id]) (clear [destVar c]) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in let t = whd_betadeltaiota (type_of (mkVar id)) in match match_with_equality_type t with @@ -2290,7 +2290,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in - let sigma, _ = Typing.e_type_of env sigma term in + let sigma, _ = Typing.type_of env sigma term in sigma, term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) @@ -2376,7 +2376,7 @@ let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.enter begin fun gl -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c)) end @@ -2459,7 +2459,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = mkProd_or_LetIn (na,b,t) cl', evd' let generalize_goal gl i ((occs,c,b),na as o) cl = - let t = pf_type_of gl c in + let t = pf_unsafe_type_of gl c in let env = pf_env gl in generalize_goal_gen env (pf_ids_of_hyps gl) i o t cl @@ -2520,7 +2520,7 @@ let new_generalize_gen_let lconstr = let (newcl, sigma), args = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, args) -> - let t = Tacmach.New.pf_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl c in let args = if Option.is_empty b then c :: args else args in generalize_goal_gen env ids i o t cl, args) 0 lconstr ((concl, sigma), []) @@ -2797,7 +2797,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = let id = match kind_of_term c with | Var id -> id | _ -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN @@ -3201,7 +3201,7 @@ let abstract_args gl generalize_vars dep id defined f args = let rel, c = Reductionops.splay_prod_n env sigma 1 prod in List.hd rel, c in - let argty = pf_type_of gl arg in + let argty = pf_unsafe_type_of gl arg in let ty = (* refresh_universes_strict *) ty in let lenctx = List.length ctx in let liftargty = lift lenctx argty in @@ -3242,7 +3242,7 @@ let abstract_args gl generalize_vars dep id defined f args = in if dogen then let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3566,13 +3566,13 @@ let guess_elim isrec dep s hyp0 gl = Tacmach.New.pf_apply build_case_analysis_scheme gl mind true s else Tacmach.New.pf_apply build_case_analysis_scheme_default gl mind s in - let elimt = Tacmach.New.pf_type_of gl elimc in + let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in - Proofview.Goal.sigma gl, (e, Tacmach.New.pf_type_of gl elimc), ind_type_guess + Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = (Id.t list * (elim_arg_kind * bool * Id.t) list) array @@ -3604,7 +3604,7 @@ let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_type_of gl (fst elimc)) in + let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -3963,7 +3963,7 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_type_of gl in + let type_of = Tacmach.New.pf_unsafe_type_of gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -4225,7 +4225,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE begin @@ -4276,7 +4276,7 @@ let prove_transitivity hdcncl eq_kind t = | HeterogenousEq (typ1,c1,typ2,c2) -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let type_of = Typing.type_of env sigma in + let type_of = Typing.unsafe_type_of env sigma in let typt = type_of t in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 96bb89e2a..f90508090 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -355,7 +355,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -417,7 +417,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let tt1 = Tacmach.New.pf_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 diff --git a/toplevel/class.ml b/toplevel/class.ml index 6a485d52c..0e270f960 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly = let _ = if not (Reductionops.is_conv_leq env Evd.empty - (Typing.type_of env Evd.empty val_f) typ_f) + (Typing.unsafe_type_of env Evd.empty val_f) typ_f) then errorlabstrm "" (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/toplevel/command.ml b/toplevel/command.ml index 1249581ee..7cf0477f9 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -847,7 +847,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in - let relty = Typing.type_of env !evdref rel in + let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = user_err_loc (constr_loc r, @@ -988,7 +988,7 @@ let interp_recursive isfix fixl notations = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then - let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in + let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in |