From 6fcbaddb882f5fdf1684ee4f1a4458e3e29b5249 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 19 Jul 2024 13:21:00 +0200 Subject: [PATCH] Rename Evd.evar_universe_context -> ustate --- dev/ml_toplevel/include_printers | 2 +- dev/top_printers.dbg | 2 +- dev/top_printers.ml | 2 +- dev/top_printers.mli | 2 +- engine/evarutil.ml | 2 +- engine/evd.ml | 8 +++++--- engine/evd.mli | 6 ++++-- engine/termops.ml | 23 ++++++----------------- engine/termops.mli | 4 +++- engine/uState.ml | 14 ++++++++++++++ engine/uState.mli | 2 ++ interp/constrintern.mli | 8 ++++---- plugins/funind/gen_principle.ml | 4 ++-- plugins/funind/recdef.ml | 2 +- plugins/ltac/leminv.ml | 2 +- plugins/ssr/ssrbwd.ml | 2 +- plugins/ssr/ssrcommon.ml | 10 +++++----- plugins/ssr/ssrelim.ml | 4 ++-- plugins/ssr/ssrequality.ml | 10 +++++----- plugins/ssr/ssrfwd.ml | 2 +- plugins/ssrmatching/ssrmatching.ml | 4 ++-- plugins/ssrmatching/ssrmatching.mli | 2 +- pretyping/detyping.ml | 4 ++-- pretyping/inductiveops.ml | 2 +- pretyping/pretyping.ml | 2 +- pretyping/pretyping.mli | 2 +- stm/partac.ml | 2 +- tactics/elimschemes.ml | 6 +++--- tactics/eqschemes.ml | 2 +- tactics/ind_tables.ml | 4 ++-- tactics/ind_tables.mli | 4 ++-- tactics/tactics.ml | 2 +- vernac/auto_ind_decl.ml | 6 +++--- vernac/classes.ml | 2 +- vernac/comFixpoint.ml | 4 ++-- vernac/comRewriteRule.ml | 4 ++-- vernac/declare.ml | 14 +++++++------- vernac/vernacentries.ml | 2 +- 38 files changed, 95 insertions(+), 84 deletions(-) diff --git a/dev/ml_toplevel/include_printers b/dev/ml_toplevel/include_printers index 56bf86705977..f604faa35fe2 100644 --- a/dev/ml_toplevel/include_printers +++ b/dev/ml_toplevel/include_printers @@ -42,7 +42,7 @@ #install_printer (* univ full subst *) Top_printers.ppuniverse_level_subst;; #install_printer Top_printers.ppqvar_subst;; #install_printer (* univ opt subst *) Top_printers.ppuniverse_opt_subst;; -#install_printer (* evar univ ctx *) Top_printers.ppevar_universe_context;; +#install_printer (* evar univ ctx *) Top_printers.ppustate;; #install_printer (* cclosure partial_subst *) Top_printers.pp_partialfsubst;; #install_printer (* reductionops partial_subst *) Top_printers.pp_partialsubst;; #install_printer (* inductive *) Top_printers.ppind;; diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 7300a116e7f4..9e6ca9c615be 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -80,7 +80,7 @@ install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst install_printer Top_printers.ppqvar_subst install_printer Top_printers.ppuniverse_level_subst -install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppustate install_printer Top_printers.ppconstraints install_printer Top_printers.ppuniverseconstraints install_printer Top_printers.ppuniverse_context_future diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 7f508b470be5..3bc37669c04e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -265,7 +265,7 @@ let ppuniverse_subst l = pp (UnivSubst.pr_universe_subst Level.raw_pr l) let ppuniverse_opt_subst l = pp (UnivFlex.pr Level.raw_pr l) let ppqvar_subst l = pp (UVars.pr_quality_level_subst QVar.raw_pr l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst Level.raw_pr l) -let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) +let ppustate l = pp (UState.pr l) let ppconstraints c = pp (Constraints.pr Level.raw_pr c) let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 910000281516..97183f53c868 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -158,7 +158,7 @@ val ppuniverse_subst : UnivSubst.universe_subst -> unit val ppuniverse_opt_subst : UState.universe_opt_subst -> unit val ppqvar_subst : Sorts.Quality.t Sorts.QVar.Map.t -> unit val ppuniverse_level_subst : Univ.universe_level_subst -> unit -val ppevar_universe_context : UState.t -> unit +val ppustate : UState.t -> unit val ppconstraints : Univ.Constraints.t -> unit val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : UVars.UContext.t Future.computation -> unit diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 5ed2875bba57..2e8a3c810220 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -78,7 +78,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=nf_evar sigma v;utj_type=t} let nf_relevance sigma r = - UState.nf_relevance (Evd.evar_universe_context sigma) r + UState.nf_relevance (Evd.ustate sigma) r let nf_named_context_evar sigma ctx = Context.Named.map_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx diff --git a/engine/evd.ml b/engine/evd.ml index cb1a9b9f98f3..f072209a196f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -334,7 +334,7 @@ let make_evar_instance_array info args = let push id c l = if isVarId id c then l else (id, c) :: l in evar_instance_array [] push info args -type 'a in_evar_universe_context = 'a * UState.t +type 'a in_ustate = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -1118,7 +1118,9 @@ let univ_rigid = UnivRigid let univ_flexible = UnivFlexible false let univ_flexible_alg = UnivFlexible true -let evar_universe_context d = d.universes +let ustate d = d.universes + +let evar_universe_context d = ustate d let universe_context_set d = UState.context_set d.universes @@ -1141,7 +1143,7 @@ let check_univ_decl_early ~poly ~with_obls sigma udecl terms = with monomorphic Program definitions.") in let vars = List.fold_left (fun acc b -> Univ.Level.Set.union acc (Vars.universes_of_constr b)) Univ.Level.Set.empty terms in - let uctx = evar_universe_context sigma in + let uctx = ustate sigma in let uctx = UState.collapse_sort_variables uctx in let uctx = UState.restrict uctx vars in ignore (UState.check_univ_decl ~poly uctx udecl) diff --git a/engine/evd.mli b/engine/evd.mli index 6ecb71cee4f2..4d0c299c8e93 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -622,7 +622,7 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -type 'a in_evar_universe_context = 'a * UState.t +type 'a in_ustate = 'a * UState.t val restrict_universe_context : ?lbound:UGraph.Bound.t -> evar_map -> Univ.Level.Set.t -> evar_map @@ -665,7 +665,9 @@ val check_constraints : evar_map -> Univ.Constraints.t -> bool val check_qconstraints : evar_map -> Sorts.QConstraints.t -> bool val check_quconstraints : evar_map -> Sorts.QUConstraints.t -> bool -val evar_universe_context : evar_map -> UState.t +val ustate : evar_map -> UState.t +val evar_universe_context : evar_map -> UState.t [@@deprecated "(8.21) Use [Evd.ustate]"] + val universe_context_set : evar_map -> Univ.ContextSet.t val sort_context_set : evar_map -> UnivGen.sort_context_set val universe_subst : evar_map -> UnivFlex.t diff --git a/engine/termops.ml b/engine/termops.ml index 98b1ac5ea678..2b61d9606284 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -296,24 +296,13 @@ let has_no_evar sigma = try let () = Evd.fold (fun _ _ () -> raise_notrace Exit) sigma () in true with Exit -> false -let pr_evd_level sigma = UState.pr_uctx_level (Evd.evar_universe_context sigma) +let pr_evd_level sigma = UState.pr_uctx_level (Evd.ustate sigma) -let pr_evd_qvar sigma = UState.pr_uctx_qvar (Evd.evar_universe_context sigma) +let pr_evd_qvar sigma = UState.pr_uctx_qvar (Evd.ustate sigma) -let reference_of_level sigma l = UState.qualid_of_level (Evd.evar_universe_context sigma) l +let reference_of_level sigma l = UState.qualid_of_level (Evd.ustate sigma) l -let pr_evar_universe_context ctx = - let open UState in - let prl = pr_uctx_level ctx in - if UState.is_empty ctx then mt () - else - v 0 (str"UNIVERSES:"++brk(0,1)++ - h (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ - UnivFlex.pr prl (UState.subst ctx) ++ fnl() ++ - str"SORTS:"++brk(0,1)++ - h (UState.pr_sort_opt_subst ctx) ++ fnl() ++ - str "WEAK CONSTRAINTS:"++brk(0,1)++ - h (UState.pr_weak prl ctx) ++ fnl ()) +let pr_evar_universe_context = UState.pr let print_env_short env sigma = let print_constr = Internal.print_kconstr in @@ -350,10 +339,10 @@ let pr_evar_constraints sigma pbs = prlist_with_sep fnl pr_evconstr pbs let pr_evar_map_gen with_univs pr_evars env sigma = - let uvs = Evd.evar_universe_context sigma in + let uvs = Evd.ustate sigma in let (_, conv_pbs) = Evd.extract_all_conv_pbs sigma in let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl () - and svs = if with_univs then pr_evar_universe_context uvs else mt () + and svs = if with_univs then UState.pr uvs else mt () and cstrs = if List.is_empty conv_pbs then mt () else diff --git a/engine/termops.mli b/engine/termops.mli index 4506c77cec26..4d7b7ca89787 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -293,7 +293,6 @@ val pr_evar_map : ?with_univs:bool -> int option -> env -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> any_evar_info -> bool) -> env -> evar_map -> Pp.t val pr_metaset : Metaset.t -> Pp.t -val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t val pr_evd_qvar : evar_map -> Sorts.QVar.t -> Pp.t @@ -320,3 +319,6 @@ val print_rel_context : env -> Evd.evar_map -> Pp.t val print_env : env -> Evd.evar_map -> Pp.t end + +val pr_evar_universe_context : UState.t -> Pp.t +[@@deprecated "(8.21) Use [Evd.pr_ustate] instead"] diff --git a/engine/uState.ml b/engine/uState.ml index eb0128487b1c..b65a76bf9310 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -1253,6 +1253,20 @@ let pr_weak prl {minim_extra={UnivMinim.weak_constraints=weak}} = let pr_sort_opt_subst uctx = QState.pr (pr_uctx_qvar uctx) uctx.sort_variables +let pr ctx = + let open Pp in + let prl = pr_uctx_level ctx in + if is_empty ctx then mt () + else + v 0 + (str"UNIVERSES:"++brk(0,1)++ + h (Univ.pr_universe_context_set prl (context_set ctx)) ++ fnl () ++ + UnivFlex.pr prl (subst ctx) ++ fnl() ++ + str"SORTS:"++brk(0,1)++ + h (pr_sort_opt_subst ctx) ++ fnl() ++ + str "WEAK CONSTRAINTS:"++brk(0,1)++ + h (pr_weak prl ctx) ++ fnl ()) + module Internal = struct diff --git a/engine/uState.mli b/engine/uState.mli index 795887e271a8..593cc3e8146b 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -264,6 +264,8 @@ val id_of_qvar : t -> Sorts.QVar.t -> Id.t option val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t +val pr : t -> Pp.t + val pr_sort_opt_subst : t -> Pp.t module Internal : diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ee8af038615e..46b321f7267e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -99,13 +99,13 @@ val intern_context : env -> bound_univs:UnivNames.universe_binders -> expecting evars and pending problems to be all resolved *) val interp_constr : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> ?impls:internalization_env -> - constr_expr -> constr Evd.in_evar_universe_context + constr_expr -> constr Evd.in_ustate val interp_casted_constr : ?flags:inference_flags -> env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types -> constr Evd.in_evar_universe_context + constr_expr -> types -> constr Evd.in_ustate val interp_type : ?flags:inference_flags -> env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types Evd.in_evar_universe_context + constr_expr -> types Evd.in_ustate (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) @@ -162,7 +162,7 @@ val interp_reference : ltac_sign -> qualid -> glob_constr (** Interpret binders *) val interp_binder : env -> evar_map -> Name.t -> constr_expr -> - types Evd.in_evar_universe_context + types Evd.in_ustate val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map * types diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 1f0ed91884f3..37e570ade1e4 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -202,7 +202,7 @@ let build_functional_principle env (sigma : Evd.evar_map) old_princ_type sorts f in let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in let ftac = proof_tac (Array.map map funs) mutr_nparams in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in let typ = EConstr.of_constr new_principle_type in let body, typ, univs, _safe, _uctx = Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac @@ -303,7 +303,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = Declare.declare_entry ~name:new_princ_name ~hook diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 7aa90b459593..371c540605ae 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1521,7 +1521,7 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes in try let sigma, new_goal_type = build_new_goal_type lemma in - let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in + let sigma = Evd.from_ctx (Evd.ustate sigma) in open_new_goal ~lemma start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) new_goal_type with EmptySubgoals -> diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 893828721e43..07389c15b70c 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -199,7 +199,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = user_err (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in + let pf = Proof.start ~name ~poly (Evd.from_ctx (ustate sigma)) [invEnv,invGoal] in let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context_val () in diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index b705fa5e6183..04b57c881b98 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -148,7 +148,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = | [], [agens] -> let sigma = Proofview.Goal.sigma gl in let clr', lemma = interp_agens ist (pf_env gl) sigma ~concl:(pf_concl gl) agens in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context (fst lemma)) in + let sigma = Evd.merge_universe_context sigma (Evd.ustate (fst lemma)) in Tacticals.tclTHENLIST [Proofview.Unsafe.tclEVARS sigma; cleartac clr; refine_with ~beta:true lemma; cleartac clr'] | _, _ -> Tacticals.tclTHENLIST [apply_top_tac; cleartac clr])) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d5c40961c773..6b4163c793df 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -399,7 +399,7 @@ let resolve_typeclasses env sigma ~where ~fail = let abs_evars env sigma0 ?(rigid = []) (sigma, c0) = let c0 = Evarutil.nf_evar sigma c0 in - let sigma0, ucst = sigma0, Evd.evar_universe_context sigma in + let sigma0, ucst = sigma0, Evd.ustate sigma in let nenv = env_size env in let abs_evar n k = let open EConstr in @@ -894,7 +894,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let uct = Evd.evar_universe_context (fst oc) in + let uct = Evd.ustate (fst oc) in let n, oc = abs_evars_pirrel env sigma oc in Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*> Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ?beta n oc) @@ -1017,7 +1017,7 @@ let get_hyp env sigma id = (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux env sigma ~concl to_ind ((oclr, occ), t) = let pat = interp_cpattern env sigma t None in (* UGLY API *) - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context @@ pat.pat_sigma) in + let sigma = Evd.merge_universe_context sigma (Evd.ustate @@ pat.pat_sigma) in let sigma, c, cl = fill_rel_occ_pattern env sigma concl pat occ in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in if not(occur_existential sigma c) then @@ -1099,7 +1099,7 @@ let abs_wgen env sigma keep_let f gen (args,c) = | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern env sigma p None in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context cp.pat_sigma) in + let sigma = Evd.merge_universe_context sigma (Evd.ustate cp.pat_sigma) in let sigma, t, c = fill_rel_occ_pattern env sigma c cp None in evar_closed t p; let ut = red_product_skip_id env sigma t in @@ -1108,7 +1108,7 @@ let abs_wgen env sigma keep_let f gen (args,c) = | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern env sigma p None in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context cp.pat_sigma) in + let sigma = Evd.merge_universe_context sigma (Evd.ustate cp.pat_sigma) in let sigma, t, c = fill_rel_occ_pattern env sigma c cp None in evar_closed t p; let sigma, ty, r = pfe_type_relevance_of env sigma t in diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 6989bd5a05c3..058372120413 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -149,7 +149,7 @@ let mkTpat env sigma0 (sigma, t) = (* takes a term, refreshes it and makes a T p let redex_of_pattern env p = match redex_of_pattern p with | None -> CErrors.anomaly (Pp.str "pattern without redex.") -| Some (sigma, e) -> Evarutil.nf_evar sigma e, Evd.evar_universe_context sigma +| Some (sigma, e) -> Evarutil.nf_evar sigma e, Evd.ustate sigma let unif_redex env sigma0 nsigma p t = (* t is a hint for the redex of p *) let t, evs, ucst = abs_evars env sigma0 (nsigma, fire_subst nsigma t) in @@ -375,7 +375,7 @@ let generate_pred env sigma0 ~concl patterns predty eqid is_rec deps elim_args n let erefl = fire_subst sigma erefl in let erefl_ty = Retyping.get_type_of env sigma erefl in let eq_ty = Retyping.get_type_of env sigma erefl_ty in - let ucst = Evd.evar_universe_context sigma in + let ucst = Evd.ustate sigma in let evds = Evar.Map.bind (Evd.find_undefined sigma) @@ Evd.evars_of_term sigma new_concl in let gen_eq_tac = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index e32d75f07870..7e94a8dadc7f 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -100,7 +100,7 @@ let congrtac ((n, t), ty) ist = debug_ssr (fun () -> (Pp.str"===congr===")); debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env env sigma concl)); let nsigma, _ as it = interp_term env sigma ist t in - let sigma = Evd.merge_universe_context sigma (Evd.evar_universe_context nsigma) in + let sigma = Evd.merge_universe_context sigma (Evd.ustate nsigma) in let f, _, _ucst = abs_evars env sigma it in let ist' = {ist with lfun = Id.Map.add pattern_id (Tacinterp.Value.of_constr f) Id.Map.empty } in @@ -457,7 +457,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ end let pf_merge_uc_of s sigma = - Evd.merge_universe_context sigma (Evd.evar_universe_context s) + Evd.merge_universe_context sigma (Evd.ustate s) let rwcltac ?under ?map_redex cl rdx dir (sigma, r) = let open Proofview.Notations in @@ -646,7 +646,7 @@ let rwrxtac ?under ?map_redex occ rdx_pat dir rule = try let ise = unify_HO env (Evd.create_evar_defs r_sigma) lhs rdx in if not (rw_progress rhs rdx ise) then raise NoMatch else - d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r) + d, (ise, Evd.ustate ise, Reductionops.nf_evar ise r) with e when CErrors.noncritical e -> rwtac rs in rwtac rules in let env0 = env in @@ -727,10 +727,10 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) (* Evarmaps below are extensions of sigma, so setting the universe context is correct *) let sigma = match rx with | None -> sigma - | Some { pat_sigma = s } -> Evd.set_universe_context sigma (Evd.evar_universe_context s) + | Some { pat_sigma = s } -> Evd.set_universe_context sigma (Evd.ustate s) in let t = interp env sigma gt in - let sigma = Evd.set_universe_context sigma (Evd.evar_universe_context (fst t)) in + let sigma = Evd.set_universe_context sigma (Evd.ustate (fst t)) in Proofview.Unsafe.tclEVARS sigma <*> (match kind with | RWred sim -> simplintac occ rx sim diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index c32b573d2293..23e1edbb2892 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -48,7 +48,7 @@ let redex_of_pattern_tc env p = | Some (sigma, e) -> sigma, e in let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in - Evarutil.nf_evar sigma e, Evd.evar_universe_context sigma + Evarutil.nf_evar sigma e, Evd.ustate sigma let ssrsettac id ((_, (pat, pty)), (_, occ)) = let open Proofview.Notations in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index a4bb08e90b5e..d399f2c6c61c 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -241,7 +241,7 @@ let nf_open_term sigma0 ise c = let c' = nf c in let _ = Evd.fold_undefined copy_def sigma0 () in let changed = sigma0 != !s' in - changed, !s', Evd.evar_universe_context ise, c' + changed, !s', Evd.ustate ise, c' let unif_end ?(solve_TC=true) env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in @@ -1295,7 +1295,7 @@ let redex_of_pattern_nf env p = | None -> CErrors.anomaly (str"pattern without redex.") | Some (sigma, e) -> sigma, e in - Evarutil.nf_evar sigma e, Evd.evar_universe_context sigma + Evarutil.nf_evar sigma e, Evd.ustate sigma let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let do_make_rel, occ = diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index a997f58afba7..f62179993bd6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -110,7 +110,7 @@ val fill_occ_pattern : ?raise_NoMatch:bool -> env -> evar_map -> EConstr.t -> pattern -> occ -> int -> - EConstr.t Evd.in_evar_universe_context * EConstr.t + EConstr.t Evd.in_ustate * EConstr.t (** Variant of the above function where we fix [h := 1] and return [redex_of_pattern pat] if [pat] has no occurrence. *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 97558c4a8abb..d73f98e19a9d 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -359,7 +359,7 @@ let { Goptions.get = print_relevances } = let detype_level_name sigma l = if Univ.Level.is_set l then GSet else - match UState.id_of_level (Evd.evar_universe_context sigma) l with + match UState.id_of_level (Evd.ustate sigma) l with | Some id -> GLocalUniv (CAst.make id) | None -> GUniv l @@ -367,7 +367,7 @@ let detype_level sigma l = UNamed (detype_level_name sigma l) let detype_qvar sigma q = - match UState.id_of_qvar (Evd.evar_universe_context sigma) q with + match UState.id_of_qvar (Evd.ustate sigma) q with | Some id -> GLocalQVar (CAst.make (Name id)) | None -> GQVar q diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d6a9ccf8bff2..1c25fed8ab5b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -275,7 +275,7 @@ let is_squashed sigma ((_,mip),u) = so here if inds=Set it is a sort poly squash (see "foo6" in test sort_poly.v) *) if Sorts.Quality.Set.for_all (fun q -> let q = UVars.subst_instance_quality u q in - let q = UState.nf_quality (Evd.evar_universe_context sigma) q in + let q = UState.nf_quality (Evd.ustate sigma) q in quality_leq q indq) squash then None else Some (SquashToQuality indq) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8f578d2cc048..87f72b057534 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1588,7 +1588,7 @@ let all_no_fail_flags = default_inference_flags false let ise_pretype_gen_ctx flags env sigma lvar kind c = let sigma, c, _ = ise_pretype_gen flags env sigma lvar kind c in - c, Evd.evar_universe_context sigma + c, Evd.ustate sigma (** Entry points of the high-level type synthesis algorithm *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 767e68f37d8b..882edfa6e715 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -136,7 +136,7 @@ val understand_ltac_ty : inference_flags -> ensure that conversion problems are all solved and that no unresolved evar remains, expanding evars. *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context + env -> evar_map -> glob_constr -> constr Evd.in_ustate val understand_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> diff --git a/stm/partac.ml b/stm/partac.ml index 64f33679970b..ac2a9ca506d2 100644 --- a/stm/partac.ml +++ b/stm/partac.ml @@ -124,7 +124,7 @@ end = struct (* {{{ *) let evars = Evarutil.undefined_evars_of_term sigma t in if Evar.Set.is_empty evars then let t = EConstr.Unsafe.to_constr t in - RespBuiltSubProof (t, Evd.evar_universe_context sigma) + RespBuiltSubProof (t, Evd.ustate sigma) else CErrors.user_err Pp.(str"The par: selector requires a tactic that makes no progress or fully" ++ diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 46de18bcfc9e..45513a1eddb9 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -30,7 +30,7 @@ let build_induction_scheme_in_type env dep sort ind = let pind = Util.on_snd EConstr.EInstance.make pind in let sigma, sort = Evd.fresh_sort_in_family ~rigid:UnivRigid sigma sort in let sigma, c = build_induction_scheme env sigma pind dep sort in - EConstr.to_constr sigma c, Evd.evar_universe_context sigma + EConstr.to_constr sigma c, Evd.ustate sigma (**********************************************************************) (* [modify_sort_scheme s rec] replaces the sort of the scheme @@ -98,7 +98,7 @@ let optimize_non_type_induction_scheme kind dep sort env _handle ind = let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma sort npars c t in let sigma = Evd.minimize_universes sigma in - (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma) + (Evarutil.nf_evars_universes sigma c', Evd.ustate sigma) | None -> build_induction_scheme_in_type env dep sort ind @@ -154,7 +154,7 @@ let build_case_analysis_scheme_in_type env dep sort ind = let sigma, sort = Evd.fresh_sort_in_family ~rigid:UnivRigid sigma sort in let (sigma, c) = build_case_analysis_scheme env sigma indu dep sort in let (c, _) = Indrec.eval_case_analysis c in - EConstr.Unsafe.to_constr c, Evd.evar_universe_context sigma + EConstr.Unsafe.to_constr c, Evd.ustate sigma let case_dep = declare_individual_scheme_object "case_dep" diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 958ad3867f99..5a142708d3f6 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -694,7 +694,7 @@ let build_r2l_rew_scheme dep env ind k = let sigma, k = Evd.fresh_sort_in_family ~rigid:UnivRigid sigma k in let (sigma, c) = build_case_analysis_scheme env sigma indu dep k in let (c, _) = Indrec.eval_case_analysis c in - EConstr.Unsafe.to_constr c, Evd.evar_universe_context sigma + EConstr.Unsafe.to_constr c, Evd.ustate sigma (**********************************************************************) (* Register the rewriting schemes *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 151ff05fe411..10f263972080 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -27,9 +27,9 @@ open Util type handle = Evd.side_effects type mutual_scheme_object_function = - Environ.env -> handle -> MutInd.t -> constr array Evd.in_evar_universe_context + Environ.env -> handle -> MutInd.t -> constr array Evd.in_ustate type individual_scheme_object_function = - Environ.env -> handle -> inductive -> constr Evd.in_evar_universe_context + Environ.env -> handle -> inductive -> constr Evd.in_ustate type 'a scheme_kind = string diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 0cf4eb882c2c..083a68237cc3 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -27,9 +27,9 @@ type scheme_dependency = | SchemeIndividualDep of inductive * individual scheme_kind type mutual_scheme_object_function = - Environ.env -> handle -> MutInd.t -> constr array Evd.in_evar_universe_context + Environ.env -> handle -> MutInd.t -> constr array Evd.in_ustate type individual_scheme_object_function = - Environ.env -> handle -> inductive -> constr Evd.in_evar_universe_context + Environ.env -> handle -> inductive -> constr Evd.in_ustate (** Main functions to register a scheme builder. Note these functions are not safe to be used by plugins as their effects won't be undone diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4b5ebe460197..e96bdd223cdc 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3360,7 +3360,7 @@ let constr_eq ~strict x y = match EConstr.eq_constr_universes env evd x y with | Some csts -> if strict then - if UState.check_universe_constraints (Evd.evar_universe_context evd) csts + if UState.check_universe_constraints (Evd.ustate evd) csts then Proofview.tclUNIT () else let info = Exninfo.reify () in diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index c5f6b2efa73f..c844f6b2a7e5 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -1172,7 +1172,7 @@ let make_bl_scheme env handle mind = let bl_goal = compute_bl_goal env handle (ind,u) lnamesparrec nparrec in let bl_goal = EConstr.of_constr bl_goal in let poly = Declareops.inductive_is_polymorphic mib in - let uctx = if poly then Evd.evar_universe_context (fst (Typing.sort_of env (Evd.from_ctx uctx) bl_goal)) else uctx in + let uctx = if poly then Evd.ustate (fst (Typing.sort_of env (Evd.from_ctx uctx) bl_goal)) else uctx in let (ans, _, _, _, uctx) = Declare.build_by_tactic ~poly env ~uctx ~typ:bl_goal (compute_bl_tact handle (ind, EConstr.EInstance.make u) lnamesparrec nparrec) in @@ -1303,7 +1303,7 @@ let make_lb_scheme env handle mind = let lb_goal = compute_lb_goal env handle (ind,u) lnamesparrec nparrec in let lb_goal = EConstr.of_constr lb_goal in let poly = Declareops.inductive_is_polymorphic mib in - let uctx = if poly then Evd.evar_universe_context (fst (Typing.sort_of env (Evd.from_ctx uctx) lb_goal)) else uctx in + let uctx = if poly then Evd.ustate (fst (Typing.sort_of env (Evd.from_ctx uctx) lb_goal)) else uctx in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly env ~uctx ~typ:lb_goal (compute_lb_tact handle ind lnamesparrec nparrec) in @@ -1496,7 +1496,7 @@ let make_eq_decidability env handle mind = Inductive.inductive_nonrec_rec_paramdecls (mib,u) in let dec_goal = EConstr.of_constr (compute_dec_goal env (ind,u) lnamesparrec nparrec) in let poly = Declareops.inductive_is_polymorphic mib in - let uctx = if poly then Evd.evar_universe_context (fst (Typing.sort_of env (Evd.from_ctx uctx) dec_goal)) else uctx in + let uctx = if poly then Evd.ustate (fst (Typing.sort_of env (Evd.from_ctx uctx) dec_goal)) else uctx in let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly env ~uctx ~typ:dec_goal (compute_dec_tact handle (ind,u) lnamesparrec nparrec) in diff --git a/vernac/classes.ml b/vernac/classes.ml index c16311b0d212..51a53fc69d8a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -333,7 +333,7 @@ let declare_instance_program pm env sigma ~locality ~poly name pri impargs udecl in let obls, _, body, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = Declare.Hook.make hook in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in let kind = Decls.IsDefinition Decls.Instance in let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~poly ~kind ~hook () in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 2068d95993e0..5ca97c8b0525 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -557,7 +557,7 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ? let bodies = List.map Option.get bodies in Evd.check_univ_decl_early ~poly ~with_obls:true sigma udecl (bodies @ fixtypes); let sigma = if poly then sigma else Evd.fix_undefined_variables sigma in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in (match fixwfs, bodies, cinfo, obls with | [Some _], [body], [cinfo], [obls] -> (* Program Fixpoint wf/measure *) @@ -569,7 +569,7 @@ let do_mutually_recursive ?pm ~program_mode ?(use_inference_hook=false) ?scope ? | None -> try let bodies = List.map Option.get bodies in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in (* All bodies are defined *) let possible_guard = (possible_guard, fixrs) in let _ : GlobRef.t list = diff --git a/vernac/comRewriteRule.ml b/vernac/comRewriteRule.ml index c5497b95417d..9b5cc205d144 100644 --- a/vernac/comRewriteRule.ml +++ b/vernac/comRewriteRule.ml @@ -424,7 +424,7 @@ let interp_rule (udecl, lhs, rhs: Constrexpr.universe_decl_expr option * _ * _) let evd = Evd.minimize_universes evd in let _qvars, uvars = EConstr.universes_of_constr evd lhs in let evd = Evd.restrict_universe_context evd uvars in - let uctx, uctx' = UState.check_univ_decl_rev (Evd.evar_universe_context evd) udecl in + let uctx, uctx' = UState.check_univ_decl_rev (Evd.ustate evd) udecl in let usubst = let inst, auctx = UVars.abstract_universes uctx' in @@ -475,7 +475,7 @@ let interp_rule (udecl, lhs, rhs: Constrexpr.universe_decl_expr option * _ * _) let _qvars', uvars' = EConstr.universes_of_constr evd' rhs in let evd' = Evd.restrict_universe_context evd' (Univ.Level.Set.union uvars uvars') in let fail pp = warn_rewrite_rules_break_SR ~loc:rhs_loc Pp.(str "universe inconsistency, missing constraints: " ++ pp) in - let () = UState.check_uctx_impl ~fail (Evd.evar_universe_context evd) (Evd.evar_universe_context evd') in + let () = UState.check_uctx_impl ~fail (Evd.ustate evd) (Evd.ustate evd') in let evd = evd' in let rhs = diff --git a/vernac/declare.ml b/vernac/declare.ml index 5da8ec1b7482..f3fe67412324 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -890,7 +890,7 @@ let prepare_definition ~info ~opaque ?using ~name ~body ~typ sigma = Option.map (interp_proof_using_gen f env sigma [name, body, typ]) using in let entry = definition_entry ~opaque ?using ~inline ?types ~univs body in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in entry, uctx let declare_definition_core ~info ~cinfo ~opaque ~obls ~body ?using sigma = @@ -920,7 +920,7 @@ let prepare_obligations ~name ?types ~body env sigma = RetrieveObl.check_evars env sigma; let body, types = EConstr.(of_constr body, of_constr types) in let obls, (_, evmap), body, cty = RetrieveObl.retrieve_obligations env name sigma 0 body types in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in body, cty, uctx, evmap, obls let prepare_parameter ~poly ~udecl ~types sigma = @@ -1621,7 +1621,7 @@ let start_proof_core ~name ~pinfo ?using sigma goals = let sign = match sign with None -> initialize_named_context_for_proof () | Some sign -> sign in (Global.env_of_context sign, typ)) goals in let proof = Proof.start ~name ~poly ?typing_flags sigma goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + let initial_euctx = Evd.ustate Proof.((data proof).sigma) in { proof ; endline_tactic = None ; using @@ -1644,7 +1644,7 @@ let start = start_core ?proof_ending:None let start_dependent ~info ~name ~proof_ending goals = let { Info.poly; typing_flags; _ } = info in let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in + let initial_euctx = Evd.ustate Proof.((data proof).sigma) in let cinfo = [] in let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in { proof @@ -1872,7 +1872,7 @@ let prepare_proof ?(warn_incomplete=true) { proof; pinfo } = else if Evd.has_undefined evd then warn_remaining_unresolved_evars () end in - proofs, Evd.evar_universe_context evd + proofs, Evd.ustate evd exception NotGuarded of Environ.env * Evd.evar_map * @@ -2067,7 +2067,7 @@ let build_by_tactic env ~uctx ~poly ~typ tac = let sign = Environ.(val_of_named_context (named_context env)) in let sigma = Evd.from_ctx uctx in let ce, status, sigma = build_constant_by_tactic ~name ~sigma ~sign ~poly typ tac in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in (* ignore side effect universes: we don't reset the global env in this code path so the side effects are still present cf #13271 and discussion in #18874 @@ -2249,7 +2249,7 @@ let save_admitted ~pm ~proof = we take the initial types *) let sigma = Evd.minimize_universes sigma in let typs = List.map (EConstr.to_constr sigma) typs in - let uctx = Evd.evar_universe_context sigma in + let uctx = Evd.ustate sigma in finish_admitted ~pm ~pinfo:proof.pinfo ~uctx ~sec_vars typs (************************************************************************) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index acbb06135c30..c4cb3a430d84 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -167,7 +167,7 @@ let show_top_evars ~proof = let show_universes ~proof = let Proof.{goals;sigma} = Proof.data proof in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in - Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ + UState.pr (Evd.ustate sigma) ++ fnl () ++ v 1 (str "Normalized constraints:" ++ cut() ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)