Rename Evd.evar_universe_context -> ustate

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;;

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

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 =

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

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

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)

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

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

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"]

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
 

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 :

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
 

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

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 ->

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

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]))

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

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 =

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

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

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 =

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. *)