diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 2 | ||||
-rw-r--r-- | vernac/comAssumption.ml | 8 | ||||
-rw-r--r-- | vernac/comFixpoint.ml | 10 | ||||
-rw-r--r-- | vernac/comInductive.ml | 22 | ||||
-rw-r--r-- | vernac/comProgramFixpoint.ml | 4 | ||||
-rw-r--r-- | vernac/obligations.ml | 6 | ||||
-rw-r--r-- | vernac/record.ml | 4 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 21 |
8 files changed, 36 insertions, 41 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 0533d0d43..cd5eff4e7 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -52,7 +52,7 @@ let _ = let open Vernacexpr in { info with hint_pattern = Option.map - (Constrintern.intern_constr_pattern (Global.env())) + (Constrintern.intern_constr_pattern (Global.env()) Evd.(from_env Global.(env()))) info.hint_pattern } in Flags.silently (fun () -> Hints.add_hints local [typeclasses_db] diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 7e5b941ad..9fd2153cb 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Vars -open Environ open Declare open Names open Globnames @@ -87,7 +86,6 @@ match local with let interp_assumption sigma env impls bl c = let c = mkCProdN ?loc:(local_binders_loc bl) bl c in let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in - let ty = EConstr.Unsafe.to_constr ty in sigma, (ty, impls) (* When monomorphic the universe constraints are declared with the first declaration only. *) @@ -151,9 +149,9 @@ let do_assumptions kind nl l = let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> let sigma,(t,imps) = interp_assumption sigma env ienv [] c in let env = - push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in + EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun {CAst.v=id} ienv -> - let impls = compute_internalization_data env Variable t imps in + let impls = compute_internalization_data env sigma Variable t imps in Id.Map.add id impls ienv) idl ienv in ((sigma,env,ienv),((is_coe,idl),t,imps))) (sigma,env,empty_internalization_env) l @@ -161,7 +159,7 @@ let do_assumptions kind nl l = let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) let sigma = Evd.nf_constraints sigma in - let nf_evar c = EConstr.to_constr sigma (EConstr.of_constr c) in + let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 489f299a2..edfe7aa81 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -212,8 +212,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let fixtypes = List.map EConstr.Unsafe.to_constr fixtypes in - let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in + let impls = compute_internalization_env env sigma Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) let sigma, fixdefs = @@ -226,10 +225,9 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in - let sigma, nf = nf_evars_and_universes sigma in - let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs in - let fixdefs = List.map (Option.map nf) fixdefs in - let fixtypes = List.map nf fixtypes in + let sigma, _ = nf_evars_and_universes sigma in + let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in + let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index c650e9e40..cef5546c6 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -11,7 +11,6 @@ open CErrors open Sorts open Util open Constr -open Termops open Environ open Declare open Names @@ -51,7 +50,7 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function ) let push_types env idl tl = - List.fold_left2 (fun env id t -> Environ.push_rel (LocalAssum (Name id,t)) env) + List.fold_left2 (fun env id t -> EConstr.push_rel (LocalAssum (Name id,t)) env) env idl tl type structured_one_inductive_expr = { @@ -90,7 +89,7 @@ let check_all_names_different indl = | _ -> raise (InductiveError (SameNamesOverlap l)) let mk_mltype_data sigma env assums arity indname = - let is_ml_type = is_sort env sigma (EConstr.of_constr arity) in + let is_ml_type = is_sort env sigma arity in (is_ml_type,indname,assums) let prepare_param = function @@ -130,14 +129,13 @@ let is_impredicative env u = u = Prop Null || (is_impredicative_set env && u = Prop Pos) let interp_ind_arity env sigma ind = - let c = intern_gen IsType env ind.ind_arity in + let c = intern_gen IsType env sigma ind.ind_arity in let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in let sigma,t = understand_tcc env sigma ~expected_type:IsType c in let pseudo_poly = check_anonymous_type c in let () = if not (Reductionops.is_arity env sigma t) then user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity") in - let t = EConstr.Unsafe.to_constr t in sigma, (t, pseudo_poly, impls) let interp_cstrs env sigma impls mldata arity ind = @@ -272,7 +270,6 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let sigma, (impls, ((env_params, ctx_params), userimpls)) = interp_context_evars env0 sigma paramsl in - let ctx_params = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx_params in let indnames = List.map (fun ind -> ind.ind_name) indl in (* Names of parameters as arguments of the inductive type (defs removed) *) @@ -282,16 +279,16 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = (* Interpret the arities *) let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in - let fullarities = List.map (fun (c, _, _) -> Term.it_mkProd_or_LetIn c ctx_params) arities in + let fullarities = List.map (fun (c, _, _) -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in let env_ar = push_types env0 indnames fullarities in - let env_ar_params = push_rel_context ctx_params env_ar in + let env_ar_params = EConstr.push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, _, impls) -> userimpls @ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in - let impls = compute_internalization_env env0 ~impls (Inductive (params,true)) indnames fullarities indimpls in - let ntn_impls = compute_internalization_env env0 (Inductive (params,true)) indnames fullarities indimpls in + let impls = compute_internalization_env env0 sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in + let ntn_impls = compute_internalization_env env0 sigma (Inductive (params,true)) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in let sigma, constructors = @@ -306,15 +303,14 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = let sigma = solve_remaining_evars all_and_fail_flags env_params sigma Evd.empty in (* Compute renewed arities *) let sigma, nf = nf_evars_and_universes sigma in - let arities = List.map nf arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in + let arities = List.map EConstr.(to_constr sigma) arities in let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in let sigma, nf' = nf_evars_and_universes sigma in - let nf x = nf' (nf x) in let arities = List.map nf' arities in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in - let ctx_params = Context.Rel.map nf ctx_params in + let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in let uctx = Evd.check_univ_decl ~poly sigma decl in List.iter (fun c -> check_evars env_params Evd.empty sigma (EConstr.of_constr c)) arities; Context.Rel.iter (fun c -> check_evars env0 Evd.empty sigma (EConstr.of_constr c)) ctx_params; diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index af34f8b29..bd7ee0978 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -171,8 +171,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, intern_body = let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in let (r, l, impls, scopes) = - Constrintern.compute_internalization_data env - Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls + Constrintern.compute_internalization_data env sigma + Constrintern.Recursive full_arity impls in let newimpls = Id.Map.singleton recname (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))], diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e4bcbc4bb..6447fc350 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -816,13 +816,13 @@ let solve_by_tac name evi t poly ctx = let id = name in let concl = EConstr.of_constr evi.evar_concl in (* spiwack: the status is dropped. *) - let (entry,_,ctx') = Pfedit.build_constant_by_tactic + let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let body, () = Future.force entry.const_entry_body in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard (Global.env ()) (fst body); + Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' let obligation_terminator name num guard hook auto pf = @@ -838,7 +838,7 @@ let obligation_terminator name num guard hook auto pf = let (body, cstr), () = Future.force entry.Entries.const_entry_body in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in - Inductiveops.control_only_guard (Global.env ()) body; + Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (** Declare the obligation ourselves and drop the hook *) let prg = get_info (ProgMap.find name !from_prg) in (** Ensure universes are substituted properly in body and type *) diff --git a/vernac/record.ml b/vernac/record.ml index 1140e3d37..44113bfad 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -70,7 +70,7 @@ let interp_fields_evars env sigma impls_env nots l = let impls = match i with | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method (EConstr.to_constr sigma t') impl) impls + | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls in let d = match b' with | None -> LocalAssum (i,t') @@ -145,7 +145,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let assums = List.filter is_local_assum newps in let params = List.map (RelDecl.get_name %> Name.get_id) assums in let ty = Inductive (params,(finite != Declarations.BiFinite)) in - let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr sigma arity] [imps] in + let impls_env = compute_internalization_env env0 sigma ~impls:impls_env ty [id] [arity] [imps] in let env2,sigma,impls,newfs,data = interp_fields_evars env_ar sigma impls_env nots (binders_of_decls fs) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 89fd2b641..6b7746db4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1025,7 +1025,9 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = let sr = smart_global reference in let inf_names = let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in - Impargs.compute_implicits_names (Global.env ()) ty + let env = Global.env () in + let sigma = Evd.from_env env in + Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) in let prev_names = try Arguments_renaming.arguments_names sr with Not_found -> inf_names @@ -1253,7 +1255,7 @@ let vernac_reserve bl = let env = Global.env() in let sigma = Evd.from_env env in let t,ctx = Constrintern.interp_type env sigma c in - let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) (EConstr.of_constr t) in + let t = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_ctx ctx) t in let t,_ = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1627,6 +1629,7 @@ let vernac_global_check c = let senv = Global.safe_env() in let uctx = UState.context_set uctx in let senv = Safe_typing.push_context_set false uctx senv in + let c = EConstr.to_constr sigma c in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in print_safe_judgment env sigma j ++ @@ -1747,10 +1750,10 @@ let interp_search_restriction = function open Search -let interp_search_about_item env = +let interp_search_about_item env sigma = function | SearchSubPattern pat -> - let _,pat = intern_constr_pattern env pat in + let _,pat = intern_constr_pattern env sigma pat in GlobSearchSubPattern pat | SearchString (s,None) when Id.is_valid s -> GlobSearchString s @@ -1796,13 +1799,13 @@ let vernac_search ~atts s gopt r = (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> snd (Pfedit.get_goal_context g) , Some g in - let get_pattern c = snd (intern_constr_pattern env c) in + let get_pattern c = snd (intern_constr_pattern env Evd.(from_env env) c) in let pr_search ref env c = let pr = pr_global ref in let pp = if !search_output_name_only then pr else begin - let pc = pr_lconstr_env env Evd.empty c in + let pc = pr_lconstr_env env Evd.(from_env env) c in hov 2 (pr ++ str":" ++ spc () ++ pc) end in Feedback.msg_notice pp @@ -1815,7 +1818,8 @@ let vernac_search ~atts s gopt r = | SearchHead c -> (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> - (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search + (Search.search_about gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + Search.prioritize_search) pr_search let vernac_locate = function | LocateAny (AN qid) -> print_located_qualid qid @@ -1910,8 +1914,7 @@ let vernac_check_guard () = let message = try let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in - Inductiveops.control_only_guard (Goal.V82.env sigma gl) - (EConstr.Unsafe.to_constr pfterm); + Inductiveops.control_only_guard (Goal.V82.env sigma gl) sigma pfterm; (str "The condition holds up to here") with UserError(_,s) -> (str ("Condition violated: ") ++s) |