diff options
31 files changed, 169 insertions, 147 deletions
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml index c5b26e6d5..5d3b2b886 100644 --- a/ltac/evar_tactics.ml +++ b/ltac/evar_tactics.ml @@ -77,7 +77,7 @@ let let_evar name typ = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in - let _ = Typing.e_sort_of env sigma typ in + let _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in let sigma = Sigma.Unsafe.of_evar_map !sigma in let id = match name with | Names.Anonymous -> diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 076e4c05e..5703687c4 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -113,7 +113,7 @@ let extends_undefined evars evars' = let app_poly_check env evars f args = let (evars, cstrs), fc = f evars in let evdref = ref evars in - let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in + let t = Typing.e_solve_evars env evdref (EConstr.of_constr (mkApp (fc, args))) in (!evdref, cstrs), t let app_poly_nocheck env evars f args = @@ -382,7 +382,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.type_of env (goalevars evars) c in + let evd', t = Typing.type_of env (goalevars evars) (EConstr.of_constr c) in (evd', cstrevars evars), c module PropGlobal = struct @@ -485,7 +485,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.unsafe_type_of env evd argl in + let ty = Typing.unsafe_type_of env evd (EConstr.of_constr 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 |]) |]))) @@ -787,7 +787,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.unsafe_type_of env (goalevars evars) appm in + let appmtype = Typing.unsafe_type_of env (goalevars evars) (EConstr.of_constr appm) in let cstrs = List.map (Option.map (fun r -> r.rew_car, get_opt_rew_rel r.rew_prf)) (Array.to_list morphobjs') @@ -1477,7 +1477,7 @@ type result = (evar_map * constr option * types) option option let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result = let evdref = ref sigma in - let sort = Typing.e_sort_of env evdref concl in + let sort = Typing.e_sort_of env evdref (EConstr.of_constr concl) in let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = @@ -1870,7 +1870,7 @@ let declare_projection n instance_id r = let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let term = proper_projection c ty in - let sigma, typ = Typing.type_of env sigma term in + let sigma, typ = Typing.type_of env sigma (EConstr.of_constr term) in let ctx, typ = decompose_prod_assum typ in let typ = let n = @@ -1902,7 +1902,7 @@ let declare_projection n instance_id r = let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in let sigma = Evd.from_ctx ctx in - let t = Typing.unsafe_type_of env sigma m in + let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in let cstrs = let rec aux t = match kind_of_term t with @@ -1932,7 +1932,7 @@ let build_morphism_signature env sigma m = let default_morphism sign m = let env = Global.env () in let sigma = Evd.from_env env in - let t = Typing.unsafe_type_of env sigma m in + let t = Typing.unsafe_type_of env sigma (EConstr.of_constr m) in let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in @@ -2126,7 +2126,7 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let (sigma, t) = Typing.type_of env sigma rel in + let (sigma, t) = Typing.type_of env sigma (EConstr.of_constr rel) in let car = RelDecl.get_type (List.hd (fst (Reduction.dest_prod env t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 34faa028f..8f5ac7e76 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -791,7 +791,7 @@ let interp_may_eval f ist env sigma = function let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in let evdref = ref sigma in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in - let c = Typing.e_solve_evars env evdref c in + let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in !evdref , c with | Not_found -> @@ -799,7 +799,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.type_of ~refresh:true env sigma c_interp + Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) | ConstrTerm c -> try f ist env sigma c diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 36a96fdb5..58454eedf 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -50,7 +50,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = e_sort_of env (ref sigma) (EConstr.of_constr c) let rec decompose_term env sigma t= match kind_of_term (whd env t) with @@ -247,7 +247,7 @@ let new_refine c = Proofview.V82.tactic (refine c) let assert_before n c = Proofview.Goal.enter { enter = begin fun gl -> - let evm, _ = Tacmach.New.pf_apply type_of gl c in + let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) end } @@ -340,7 +340,7 @@ let refute_tac c t1 t2 p = end } let refine_exact_check c gl = - let evm, _ = pf_apply type_of gl c in + let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl let convert_to_goal_tac c t1 t2 p = @@ -480,10 +480,10 @@ let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> Proofview.Goal.enter { enter = begin fun gl -> let open Tacmach.New in - let evm, ty = pf_apply type_of gl c1 in + let evm, ty = pf_apply type_of gl (EConstr.of_constr c1) in let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm (EConstr.of_constr ty) in let term = mkApp (fc, [| ty; c1; c2 |]) in - let evm, _ = type_of (pf_env gl) evm term in + let evm, _ = type_of (pf_env gl) evm (EConstr.of_constr term) in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) end }) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index c17c8dbb8..dcebf7806 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -429,7 +429,7 @@ let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in + let sort = family_of_sort (Typing.e_sort_of env (ref evd) (EConstr.of_constr concl)) in let rec aux env avoid subst = function [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> @@ -437,7 +437,7 @@ let concl_refiner metas body gls = let x = id_of_name_using_hdchar env _A Anonymous in let _x = fresh_id avoid x gls in let nenv = Environ.push_named (LocalAssum (_x,_A)) env in - let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in + let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) (EConstr.of_constr _A)) in let nsubst = (n,mkVar _x)::subst in if List.is_empty rest then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index a3513692c..44bdb585a 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq= it_mkLambda_or_LetIn (mkApp(idc,[|ot|])) rc in let evmap, _ = - try Typing.type_of (pf_env gl) evmap gt + try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt) with e when CErrors.noncritical e -> error "Untypable instance, maybe higher-order non-prenex quantification" in tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 340dd2c28..0a7938069 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -329,7 +329,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) 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.type_of g to_refine in + let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g ) in @@ -544,7 +544,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.unsafe_type_of env sigma (EConstr.mkVar hyp_id)), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -639,7 +639,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.type_of g c in + let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in tclTHENLIST[ Refiner.tclEVARS evm; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c); @@ -968,7 +968,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.type_of ~refresh:true (Global.env ()) evd f + let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in decompose_prod_n_assum (nb_params + nb_args) t,evd @@ -1039,7 +1039,7 @@ 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 _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr res) in res in let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9637632a6..4b47b83af 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -283,7 +283,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 _ = Typing.e_type_of ~refresh:true (Global.env ()) evd new_principle_type in + let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof @@ -337,7 +337,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',s = Evd.fresh_sort_in_family env evd' 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.type_of ~refresh:true (Global.env ()) evd' value) in + let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( @@ -488,7 +488,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con in let _ = evd := sigma in let l_schemes = - List.map (Typing.unsafe_type_of env sigma) schemes + List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma) schemes in let i = ref (-1) in let sorts = @@ -616,7 +616,7 @@ 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 _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in (destConst f,sort) ) fas @@ -666,7 +666,7 @@ let build_case_scheme fa = Indrec.build_case_analysis_scheme_default env sigma ind sf in let sigma = Sigma.to_evar_map sigma in - let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in + let scheme_type = (Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme) in let sorts = (fun (_,_,x) -> Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 92de4d873..38cd21684 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -503,7 +503,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.from_env env) rt in - let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in + let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -611,7 +611,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.from_env env) v in - let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in + let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in let new_env = match n with Anonymous -> env @@ -627,7 +627,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.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) with Not_found -> @@ -659,7 +659,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.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ) with Not_found -> @@ -706,7 +706,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.from_env env) case_arg in - Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr + Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr) ) el in (****** The next works only if the match is not dependent ****) @@ -753,7 +753,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.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id) + Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = Detyping.detype false [] @@ -807,7 +807,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.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = Detyping.detype false [] new_env (Evd.from_env env) typ_of_id in @@ -1121,7 +1121,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in - let type_t' = Typing.unsafe_type_of env evd t' in + let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1272,7 +1272,7 @@ let do_build_inductive let evd,env = Array.fold_right2 (fun id c (evd,env) -> - let evd,t = Typing.type_of env evd (mkConstU c) in + let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in evd, Environ.push_named (LocalAssum (id,t)) (* try *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a264c37c5..0743fc5d9 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -369,7 +369,7 @@ 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 princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in Functional_principles_types.generate_functional_principle evd interactive_proof diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 9abe60402..e5286fb1f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -134,7 +134,7 @@ let generate_type evd g_to_f f graph i = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd graph))) in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in let ctxt,_ = decompose_prod_assum graph_arity in let fun_ctxt,res_type = match ctxt with @@ -202,7 +202,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.type_of ~refresh:true (Global.env ()) evd' rect_lemma in + let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in evd:=evd'; rect_lemma,typ @@ -449,7 +449,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.type_of ~refresh:true) gl term in + let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl (EConstr.of_constr term) in Proofview.V82.of_tactic (apply term) gl') )) (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) @@ -792,7 +792,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 _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in + let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 4fd9e0ff8..12ed758ba 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -657,7 +657,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.type_of (pf_env gl) (project gl) c in + let evars, ty = Typing.type_of (pf_env gl) (project gl) (EConstr.of_constr c) in tclTHEN (Refiner.tclEVARS evars) (tac ty) gl let pf_typel l tac = diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e1b95ddbc..b0a3e839b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -493,8 +493,8 @@ let ring_equality env evd (r,add,mul,opp,req) = match opp with Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|] | None -> plapp evd coq_eq_smorph [|r;add;mul|] in - let setoid = Typing.e_solve_evars env evd setoid in - let op_morph = Typing.e_solve_evars env evd op_morph in + let setoid = Typing.e_solve_evars env evd (EConstr.of_constr setoid) in + let op_morph = Typing.e_solve_evars env evd (EConstr.of_constr op_morph) in (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in @@ -581,7 +581,7 @@ let make_hyp_list env evd lH = (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH (plapp evd coq_nil [|carrier|]) in - let l' = Typing.e_solve_evars env evd l in + let l' = Typing.e_solve_evars env evd (EConstr.of_constr l) in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = @@ -707,7 +707,7 @@ let make_term_list env evd carrier rl = let l = List.fold_right (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl (plapp evd coq_nil [|carrier|]) - in Typing.e_solve_evars env evd l + in Typing.e_solve_evars env evd (EConstr.of_constr l) let carg = Tacinterp.Value.of_constr let tacarg expr = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 04f50d50e..882c052f6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1381,7 +1381,7 @@ and match_current pb (initial,tomatch) = let case = make_case_or_project pb.env indf ci pred current brvals in - Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; + Typing.check_allowed_sort pb.env !(pb.evdref) mind (EConstr.of_constr current) (EConstr.of_constr pred); { uj_val = applist (case, inst); uj_type = prod_applist typ inst } @@ -1684,7 +1684,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.type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref (EConstr.of_constr t) in evdref := evd; (t,tt) in let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in @@ -1920,7 +1920,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = assert (len == 0); let p = predicate 0 c in let env' = List.fold_right push_rel_context arsign env in - try let sigma' = fst (Typing.type_of env' sigma p) in + try let sigma' = fst (Typing.type_of env' sigma (EConstr.of_constr p)) in Some (sigma', p) with e when precatchable_exception e -> None @@ -2041,7 +2041,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty)) with Not_found -> error_case_not_inductive env !evdref - {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref (EConstr.of_constr 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; @@ -2242,7 +2242,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon (EConstr.of_constr 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.type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref (EConstr.of_constr bbody) in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 0ea6758a7..04e235cc5 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -188,7 +188,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) (fun x -> eq_app (co x)) else Some (fun x -> - let term = co x in + let term = EConstr.of_constr (co x) in Typing.e_solve_evars env evdref term) in if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then @@ -297,16 +297,16 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in (try subco () with NoSubtacCoercion -> - let typ = Typing.unsafe_type_of env evm c in - let typ' = Typing.unsafe_type_of env evm c' in + let typ = Typing.unsafe_type_of env evm (EConstr.of_constr c) in + let typ' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in coerce_application typ typ' c c' l l') else subco () | 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.unsafe_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 (EConstr.of_constr c) in + let lam_type' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in coerce_application lam_type lam_type' c c' l l' else subco () | _ -> subco ()) @@ -337,7 +337,7 @@ let app_coercion env evdref coercion v = match coercion with | None -> v | Some f -> - let v' = Typing.e_solve_evars env evdref (f v) in + let v' = Typing.e_solve_evars env evdref (EConstr.of_constr (f v)) in whd_betaiota !evdref (EConstr.of_constr v') let coerce_itf loc env evd v t c1 = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 570f95324..28ba60812 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -507,7 +507,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.unsafe_type_of env.ExtraEnv.env evd c in + let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in make_judge c ty let judge_of_Type loc evd s = @@ -644,7 +644,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; + Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj; let ftys = Array.map (nf_evar !evdref) ftys in let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in let fixj = match fixkind with @@ -898,7 +898,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } @@ -917,7 +917,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p); obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) @@ -981,7 +981,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred); mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 290d77b1b..a3983737d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1164,7 +1164,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> let sigma = Sigma.to_evar_map sigma in let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in try - let _ = Typing.unsafe_type_of env sigma abstr_trm in + let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma) 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 64264cf08..c948f9b9a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -20,6 +20,11 @@ open Typeops open Arguments_renaming open Context.Rel.Declaration +let push_rec_types pfix env = + let (i, c, t) = pfix in + let inj c = EConstr.Unsafe.to_constr c in + push_rec_types (i, Array.map inj c, Array.map inj t) env + let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -28,12 +33,12 @@ let meta_type evd mv = let constant_type_knowing_parameters env cst jl = let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - type_of_constant_knowing_parameters_in env cst paramstyp + EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp) let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp + EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp) let e_type_judgment env evdref j = match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with @@ -44,7 +49,7 @@ let e_type_judgment env evdref j = | _ -> error_not_type env j let e_assumption_of_judgment env evdref j = - try (e_type_judgment env evdref j).utj_val + try EConstr.of_constr (e_type_judgment env evdref j).utj_val with TypeError _ -> error_assumption env j @@ -84,27 +89,28 @@ let max_sort l = if Sorts.List.mem InSet l then InSet else InProp let e_is_correct_arity env evdref c pj ind specif params = + let open EConstr in let arsign = make_arity_signature env true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in let error () = error_elim_arity env ind allowed_sorts c pj None in let rec srec env pt ar = - let pt' = whd_all env !evdref (EConstr.of_constr pt) in - match kind_of_term pt', ar with + let pt' = EConstr.of_constr (whd_all env !evdref pt) in + match EConstr.kind !evdref pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error (); - srec (push_rel (LocalAssum (na1,a1)) env) t ar' + if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error (); + srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar' | Sort s, [] -> if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () | Evar (ev,_), [] -> let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in - evdref := Evd.define ev (mkSort s) evd + evdref := Evd.define ev (Constr.mkSort s) evd | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' + srec (push_rel d env) (Vars.lift 1 pt') ar' | _ -> error () in - srec env pj.uj_type (List.rev arsign) + srec env (EConstr.of_constr pj.uj_type) (List.rev arsign) let e_type_case_branches env evdref (ind,largs) pj c = let specif = lookup_mind_specif env (fst ind) in @@ -128,24 +134,25 @@ let e_judge_of_case env evdref ci pj cj lfj = uj_type = rslty } let check_type_fixpoint loc env evdref lna lar vdefj = + let open EConstr in let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type) - (EConstr.of_constr (lift lt lar.(i)))) then + (Vars.lift lt lar.(i))) then Pretype_errors.error_ill_typed_rec_body ~loc env !evdref - i lna vdefj lar + i lna vdefj (Array.map EConstr.Unsafe.to_constr lar) done (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in + let pj = Retyping.get_judgment_of env sigma p in let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in - error_elim_arity env ind sorts c pj + error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj (Some(ksort,s,error_elim_explain ksort s)) let e_judge_of_cast env evdref cj k tj = @@ -160,21 +167,36 @@ let enrich_env env evdref = let penv' = Pre_env.({ penv with env_stratification = { penv.env_stratification with env_universes = Evd.universes !evdref } }) in Environ.env_of_pre_env penv' + +let check_fix env sigma pfix = + let inj c = EConstr.to_constr sigma c in + let (idx, (ids, cs, ts)) = pfix in + check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts)) + +let check_cofix env sigma pcofix = + let inj c = EConstr.to_constr sigma c in + let (idx, (ids, cs, ts)) = pcofix in + check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts)) + +let make_judge c ty = + make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty) (* The typing machine with universes and existential variables. *) (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env evdref cstr = - match kind_of_term cstr with + let open EConstr in + let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in + match EConstr.kind !evdref cstr with | Meta n -> - { uj_val = cstr; uj_type = meta_type !evdref n } + { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n } | Evar ev -> - let ty = Evd.existential_type !evdref ev in - let jty = execute env evdref (whd_evar !evdref ty) in + let ty = EConstr.existential_type !evdref ev in + let jty = execute env evdref ty in let jty = e_assumption_of_judgment env evdref jty in - { uj_val = cstr; uj_type = jty } + { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty } | Rel n -> judge_of_relative env n @@ -183,13 +205,13 @@ let rec execute env evdref cstr = judge_of_variable env id | Const c -> - make_judge cstr (rename_type_of_constant env c) + make_judge cstr (EConstr.of_constr (rename_type_of_constant env c)) | Ind ind -> - make_judge cstr (rename_type_of_inductive env ind) + make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind)) | Construct cstruct -> - make_judge cstr (rename_type_of_constructor env cstruct) + make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct)) | Case (ci,p,c,lf) -> let cj = execute env evdref c in @@ -200,13 +222,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env fix; + check_fix env !evdref fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix env !evdref cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> @@ -222,7 +244,7 @@ let rec execute env evdref cstr = | App (f,args) -> let jl = execute_array env evdref args in let j = - match kind_of_term f with + match EConstr.kind !evdref f with | Ind ind when Environ.template_polymorphic_pind ind env -> (* Sort-polymorphism of inductive types *) make_judge f @@ -273,7 +295,7 @@ and execute_recdef env evdref (names,lar,vdef) = let lara = Array.map (e_assumption_of_judgment env evdref) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in - let vdefv = Array.map j_val vdefj in + let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) @@ -282,8 +304,8 @@ and execute_array env evdref = Array.map (execute env evdref) let e_check env evdref c t = let env = enrich_env env evdref in let j = execute env evdref c in - if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then - error_actual_type env j (nf_evar !evdref t) + if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then + error_actual_type env j (EConstr.to_constr !evdref t) (* Type of a constr *) @@ -328,4 +350,4 @@ let e_solve_evars env evdref c = (* side-effect on evdref *) nf_evar !evdref c -let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c))) +let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c)) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 04e5e40bc..3c1c4324d 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -14,33 +14,33 @@ open Evd and universes. *) (** Typecheck a term and return its type. May trigger an evarmap leak. *) -val unsafe_type_of : env -> evar_map -> constr -> types +val unsafe_type_of : env -> evar_map -> EConstr.constr -> types (** Typecheck a term and return its type + updated evars, optionally refreshing universes *) -val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types +val type_of : ?refresh:bool -> env -> evar_map -> EConstr.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 +val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val e_check : env -> evar_map ref -> constr -> types -> unit +val e_check : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) -val e_solve_evars : env -> evar_map ref -> constr -> constr +val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) -val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> +val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr -> unit (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit + Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ac2f14051..f418dc6a9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -102,7 +102,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.type_of env evd p + try Typing.type_of env evd (EConstr.of_constr p) with | UserError _ -> error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None @@ -1214,7 +1214,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c = apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' | _ -> error "Apply_Head_Then" in - apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd + apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) (EConstr.of_constr c)) Sigma.refl evd let is_mimick_head ts f = match kind_of_term f with diff --git a/proofs/clenv.ml b/proofs/clenv.ml index f4ac094b8..c2130a64a 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -29,7 +29,7 @@ open Sigma.Notations (* Abbreviations *) let pf_env = Refiner.pf_env -let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma c +let pf_type_of gls c = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c) (******************************************************************) (* Clausal environments *) diff --git a/proofs/logic.ml b/proofs/logic.ml index 2df626e1c..93b31ced1 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -86,7 +86,7 @@ let apply_to_hyp check sign id f = else sign let check_typability env sigma c = - if !check then let _ = unsafe_type_of env sigma c in () + if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () (************************************************************************) (************************************************************************) @@ -330,7 +330,7 @@ let meta_free_prefix sigma a = with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = - if !check then unsafe_type_of env sigma c + if !check then unsafe_type_of env sigma (EConstr.of_constr c) else Retyping.get_type_of env sigma (EConstr.of_constr c) let rec mk_refgoals sigma goal goalacc conclty trm = diff --git a/proofs/refine.ml b/proofs/refine.ml index e6e3ef47d..b62f0bea4 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -28,12 +28,12 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = NamedDecl.get_type decl in + let t = EConstr.of_constr (NamedDecl.get_type decl) in let evdref = ref sigma in let _ = Typing.e_sort_of env evdref t in let () = match decl with | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref body t + | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t in (!evdref, Environ.push_named decl env) in @@ -42,12 +42,12 @@ let typecheck_evar ev env sigma = let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in + let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in !evdref let typecheck_proof c concl env sigma = let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in + let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in !evdref let (pr_constrv,pr_constr) = diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b63b2ce28..148f9d675 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -93,8 +93,8 @@ 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_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 let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV @@ -175,10 +175,10 @@ module New = struct let pf_concl = Proofview.Goal.concl let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl t + pf_apply unsafe_type_of gl (EConstr.of_constr t) let pf_type_of gl t = - pf_apply type_of gl t + pf_apply type_of gl (EConstr.of_constr t) let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 46600cdd7..80b9ec06e 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -272,7 +272,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.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 + Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) @@ -290,7 +290,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.unsafe_type_of env sigma c in + let ctype = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 17038e42d..58c86ff42 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1085,7 +1085,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty))); let sigdata = find_sigma_data env (get_sort_of env sigma (EConstr.of_constr rty)) in - let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in + let sigma, a = type_of ~refresh:true env sigma (EConstr.mkRel lind) in let na = Context.Rel.Declaration.get_name (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 @@ -1119,7 +1119,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, unsafe_type_of env sigma (mkRel i))) + let folder rels i = snd (minimalrec_free_rels_rec rels (c, unsafe_type_of env sigma (EConstr.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 @@ -1165,7 +1165,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 = unsafe_type_of env sigma dflt in + let dflt_typ = unsafe_type_of env sigma (EConstr.of_constr dflt) in try let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in @@ -1184,7 +1184,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (destEvar ev) with | Some w -> - let w_type = unsafe_type_of env sigma w in + let w_type = unsafe_type_of env sigma (EConstr.of_constr w) in if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr 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]) @@ -1273,7 +1273,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,unsafe_type_of env sigma c) + | [] -> make_iterated_tuple env sigma dflt (c,unsafe_type_of env sigma (EConstr.of_constr c)) | ((sp,cnum),argnum)::l -> try let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in @@ -1367,7 +1367,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.type_of env sigma pf in + let sigma, pf_typ = Typing.type_of env sigma (EConstr.of_constr 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 @@ -1555,8 +1555,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 (EConstr.of_constr expected_goal) in (* Retype to get universes right *) - let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in - let sigma, _ = Typing.type_of env sigma body in + let sigma, expected_goal_ty = Typing.type_of env sigma (EConstr.of_constr expected_goal) in + let sigma, _ = Typing.type_of env sigma (EConstr.of_constr body) in Sigma.Unsafe.of_pair ((body, expected_goal), sigma) (* Like "replace" but decompose dependent equalities *) diff --git a/tactics/hints.ml b/tactics/hints.ml index 2aa434777..63d10573a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -910,7 +910,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 (EConstr.of_constr (unsafe_type_of env sigma c)) in + let t = hnf_constr env sigma (EConstr.of_constr (unsafe_type_of env sigma (EConstr.of_constr c))) in let hd = head_of_constr_reference (head_constr sigma t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; diff --git a/tactics/inv.ml b/tactics/inv.ml index 38f75995b..9282af759 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.type_of env) evd refl in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr 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.type_of env) evd predicate in + let _ = Evarutil.evd_comb1 (Typing.type_of env) evd (EConstr.of_constr predicate) in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c2163a274..8fb47b994 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -210,7 +210,7 @@ let convert_concl ?(check=true) ty k = let Sigma ((), sigma, p) = if check then begin let sigma = Sigma.to_evar_map sigma in - ignore (Typing.unsafe_type_of env sigma ty); + ignore (Typing.unsafe_type_of env sigma (EConstr.of_constr ty)); let sigma,b = Reductionops.infer_conv env sigma ty conclty in if not b then error "Not convertible."; Sigma.Unsafe.of_pair ((), sigma) @@ -827,7 +827,7 @@ let change_on_subterm cv_pb deep t where = { e_redfun = begin fun env sigma c -> env sigma c in if !mayneedglobalcheck then begin - try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) c) + try ignore (Typing.unsafe_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c)) with e when catchable_exception e -> error "Replacement would lead to an ill-typed term." end; @@ -1228,7 +1228,7 @@ let cut c = let is_sort = try (** Backward compat: ensure that [c] is well-typed. *) - let typ = Typing.unsafe_type_of env sigma c in + let typ = Typing.unsafe_type_of env sigma (EConstr.of_constr c) in let typ = whd_all env sigma (EConstr.of_constr typ) in match kind_of_term typ with | Sort _ -> true @@ -1940,7 +1940,7 @@ let exact_check c = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in - let sigma, ct = Typing.type_of env sigma c in + let sigma, ct = Typing.type_of env sigma (EConstr.of_constr c) in let tac = Tacticals.New.tclTHEN (convert_leq ct concl) (exact_no_check c) in @@ -2009,20 +2009,20 @@ exception DependsOnBody of Id.t option let check_is_type env sigma ty = let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in + let _ = Typing.e_sort_of env evdref (EConstr.of_constr ty) in !evdref with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in - let ty = NamedDecl.get_type decl in + let ty = EConstr.of_constr (NamedDecl.get_type decl) in let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in let _ = match decl with | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + | LocalDef (_,c,_) -> Typing.e_check env evdref (EConstr.of_constr c) ty in !evdref with e when CErrors.noncritical e -> @@ -2622,7 +2622,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in let sigma = Sigma.to_evar_map sigma in - let sigma, _ = Typing.type_of env sigma term in + let sigma, _ = Typing.type_of env sigma (EConstr.of_constr term) in let ans = term, Tacticals.New.tclTHEN (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) @@ -2783,7 +2783,7 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let env = Tacmach.pf_env gl in let ids = Tacmach.pf_ids_of_hyps gl in - let sigma, t = Typing.type_of env sigma c in + let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in generalize_goal_gen env sigma ids i o t cl let old_generalize_dep ?(with_let=false) c gl = @@ -2818,7 +2818,7 @@ let old_generalize_dep ?(with_let=false) c gl = let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in (** Check that the generalization is indeed well-typed *) - let (evd, _) = Typing.type_of env evd cl'' in + let (evd, _) = Typing.type_of env evd (EConstr.of_constr cl'') in let args = Context.Named.to_instance to_quantify_rev in tclTHENLIST [tclEVARS evd; @@ -2836,7 +2836,7 @@ let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in - let (evd, _) = Typing.type_of env evd newcl in + let (evd, _) = Typing.type_of env evd (EConstr.of_constr newcl) in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in let tac = apply_type newcl (List.map_filter map lconstr) in Sigma.Unsafe.of_pair (tac, evd) @@ -2853,7 +2853,7 @@ let new_generalize_gen_let lconstr = let newcl, sigma, args = List.fold_right_i (fun i ((_,c,b),_ as o) (cl, sigma, args) -> - let sigma, t = Typing.type_of env sigma c in + let sigma, t = Typing.type_of env sigma (EConstr.of_constr c) in let args = if Option.is_empty b then c :: args else args in let cl, sigma = generalize_goal_gen env sigma ids i o t cl in (cl, sigma, args)) @@ -4738,7 +4738,7 @@ let prove_transitivity hdcncl eq_kind t = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let type_of = Typing.unsafe_type_of env sigma in - let typt = type_of t in + let typt = type_of (EConstr.of_constr t) in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) in diff --git a/toplevel/class.ml b/toplevel/class.ml index 5aa000b16..86fd4d9a2 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -206,7 +206,7 @@ let build_id_coercion idf_opt source poly = let _ = if not (Reductionops.is_conv_leq env sigma - (EConstr.of_constr (Typing.unsafe_type_of env sigma val_f)) (EConstr.of_constr typ_f)) + (EConstr.of_constr (Typing.unsafe_type_of env sigma (EConstr.of_constr val_f))) (EConstr.of_constr typ_f)) then user_err (strbrk "Cannot be defined as coercion (maybe a bad number of arguments).") diff --git a/toplevel/command.ml b/toplevel/command.ml index 14a45f837..c6dd3eb99 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -953,7 +953,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let relty = Typing.unsafe_type_of env !evdref rel in + let relty = Typing.unsafe_type_of env !evdref (EConstr.of_constr rel) in let relargty = let error () = user_err ~loc:(constr_loc r) @@ -1034,7 +1034,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof; prop |]) in - let def = Typing.e_solve_evars env evdref def in + let def = Typing.e_solve_evars env evdref (EConstr.of_constr def) in let _ = evdref := Evarutil.nf_evar_map !evdref in let def = mkApp (def, [|intern_body_lam|]) in let binders_rel = nf_evar_context !evdref binders_rel in @@ -1105,11 +1105,11 @@ 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.type_of ~refresh:true env) evdref t in + let sort = Evarutil.evd_comb1 (Typing.type_of ~refresh:true env) evdref (EConstr.of_constr t) in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in - Typing.e_solve_evars env evdref app + Typing.e_solve_evars env evdref (EConstr.of_constr app) with e when CErrors.noncritical e -> t in LocalAssum (id,fixprot) :: env' |