aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml38
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/classes.mli2
-rw-r--r--vernac/comDefinition.ml5
-rw-r--r--vernac/comHints.ml1
-rw-r--r--vernac/comInductive.ml2
-rw-r--r--vernac/declare.ml2
-rw-r--r--vernac/declareUniv.ml68
-rw-r--r--vernac/declareUniv.mli9
-rw-r--r--vernac/himsg.ml38
-rw-r--r--vernac/metasyntax.ml12
-rw-r--r--vernac/prettyp.ml2
-rw-r--r--vernac/record.ml6
-rw-r--r--vernac/vernacentries.ml70
14 files changed, 200 insertions, 61 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 848cd501c6..9c5f111e28 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -165,6 +165,31 @@ let label_of = let open GlobRef in function
| ConstructRef ((kn,_),_) -> MutInd.label kn
| VarRef id -> Label.of_id id
+let fold_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (_,c) -> f n acc c
+ | Evar (_,l) -> List.fold_left (f n) acc l
+ | Case (ci, u, pms, p, iv, c, bl) ->
+ let mib = lookup_mind (fst ci.ci_ind) in
+ let (ci, p, iv, c, bl) = Inductive.expand_case_specif mib (ci, u, pms, p, iv, c, bl) in
+ Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty
+
let rec traverse current ctx accu t =
let open GlobRef in
match Constr.kind t with
@@ -179,20 +204,19 @@ let rec traverse current ctx accu t =
| Construct (((mind, _), _) as cst, _) ->
traverse_inductive accu mind (ConstructRef cst)
| Meta _ | Evar _ -> assert false
-| Case (_,oty,_,c,[||]) ->
+| Case (_, _, _, ([|_|], oty), _, c, [||]) when Vars.noccurn 1 oty ->
(* non dependent match on an inductive with no constructors *)
- begin match Constr.(kind oty, kind c) with
- | Lambda(_,_,oty), Const (kn, _)
- when Vars.noccurn 1 oty &&
- not (Declareops.constant_has_body (lookup_constant kn)) ->
+ begin match Constr.kind c with
+ | Const (kn, _)
+ when not (Declareops.constant_has_body (lookup_constant kn)) ->
let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
- Constr.fold_with_full_binders
+ fold_with_full_binders
Context.Rel.add (traverse current) ctx accu t
end
-| _ -> Constr.fold_with_full_binders
+| _ -> fold_with_full_binders
Context.Rel.add (traverse current) ctx accu t
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f715459616..cc59a96834 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -351,13 +351,13 @@ let build_beq_scheme mode kn =
done;
ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
- (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
- mkVar (Id.of_string "Y") ,ar2))
+ (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
+ NoInvert, mkVar (Id.of_string "Y") ,ar2))))
(constrsi.(i).cs_args))
done;
mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) (
mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) (
- mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
+ mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
in (* build_beq_scheme *)
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e1816fb138..89ff4e6939 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -81,7 +81,7 @@ val add_class : env -> Evd.evar_map -> typeclass -> unit
(** Setting opacity *)
-val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
+val set_typeclass_transparency : Tacred.evaluable_global_reference -> bool -> bool -> unit
(** For generation on names based on classes only *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c54adb45f9..b3ffb864f2 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -69,9 +69,10 @@ let protect_pattern_in_binder bl c ctypopt =
| LetIn (x,b,t,c) ->
let evd,c = aux (push_rel (LocalDef (x,b,t)) env) evd c in
evd, mkLetIn (x,t,b,c)
- | Case (ci,p,iv,a,bl) ->
+ | Case (ci,u,pms,p,iv,a,bl) ->
+ let (ci, p, iv, a, bl) = EConstr.expand_case env evd (ci, u, pms, p, iv, a, bl) in
let evd,bl = Array.fold_left_map (aux env) evd bl in
- evd, mkCase (ci,p,iv,a,bl)
+ evd, mkCase (EConstr.contract_case env evd (ci, p, iv, a, bl))
| Cast (c,_,_) -> f env evd c (* we remove the cast we had set *)
(* This last case may happen when reaching the proof of an
impossible case, as when pattern-matching on a vector of length 1 *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index f642411fa4..1c36e10e83 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -76,6 +76,7 @@ let warn_deprecated_hint_constr =
*)
let soft_evaluable =
let open GlobRef in
+ let open Tacred in
function
| ConstRef c -> EvalConstRef c
| VarRef id -> EvalVarRef id
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2be6097184..a91771f22d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -492,7 +492,7 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
end)
sigma args
| _ -> Termops.fold_constr_with_full_binders
- sigma
+ env sigma
(fun d (env,k) -> EConstr.push_rel d env, k+1)
aux envk sigma c
in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index fafee13bf6..c715304419 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -883,7 +883,7 @@ let shrink_body c ty =
(* Saving an obligation *)
(***********************************************************************)
-let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+let unfold_entry cst = Hints.HintsUnfoldEntry [Tacred.EvalConstRef cst]
let add_hint local prg cst =
let locality = if local then Goptions.OptLocal else Goptions.OptExport in
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 1987d48e0f..91ab17575d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -9,6 +9,8 @@
(************************************************************************)
open Names
+open Declarations
+open Univ
(* object_kind , id *)
exception AlreadyDeclared of (string option * Id.t)
@@ -72,25 +74,57 @@ let input_univ_names : universe_name_decl -> Libobject.obj =
subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
+let input_univ_names (src, l) =
+ if CList.is_empty l then ()
+ else Lib.add_anonymous_leaf (input_univ_names (src, l))
+
+let invent_name (named,cnt) u =
+ let rec aux i =
+ let na = Id.of_string ("u"^(string_of_int i)) in
+ if Id.Map.mem na named then aux (i+1)
+ else na, (Id.Map.add na u named, i+1)
+ in
+ aux cnt
+
+let label_and_univs_of = let open GlobRef in function
+ | ConstRef c ->
+ let l = Label.to_id @@ Constant.label c in
+ let univs = (Global.lookup_constant c).const_universes in
+ l, univs
+ | IndRef (c,_) ->
+ let l = Label.to_id @@ MutInd.label c in
+ let univs = (Global.lookup_mind c).mind_universes in
+ l, univs
+ | VarRef id ->
+ CErrors.anomaly ~label:"declare_univ_binders"
+ Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
+ | ConstructRef _ ->
+ CErrors.anomaly ~label:"declare_univ_binders"
+ Pp.(str "declare_univ_binders on a constructor reference")
+
let declare_univ_binders gr pl =
- if Global.is_polymorphic gr then
- ()
- else
- let l = let open GlobRef in match gr with
- | ConstRef c -> Label.to_id @@ Constant.label c
- | IndRef (c, _) -> Label.to_id @@ MutInd.label c
- | VarRef id ->
- CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".")
- | ConstructRef _ ->
- CErrors.anomaly ~label:"declare_univ_binders"
- Pp.(str "declare_univ_binders on a constructor reference")
+ let l, univs = label_and_univs_of gr in
+ match univs with
+ | Polymorphic _ -> ()
+ | Monomorphic (levels,_) ->
+ (* First the explicitly named universes *)
+ let named, univs = Id.Map.fold (fun id univ (named,univs) ->
+ let univs = match Univ.Level.name univ with
+ | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
+ | Some univ -> (id,univ)::univs
+ in
+ let named = LSet.add univ named in
+ named, univs)
+ pl (LSet.empty,[])
in
- let univs = Id.Map.fold (fun id univ univs ->
- match Univ.Level.name univ with
- | None -> assert false (* having Prop/Set/Var as binders is nonsense *)
- | Some univ -> (id,univ)::univs) pl []
+ (* then invent names for the rest *)
+ let _, univs = LSet.fold (fun univ (aux,univs) ->
+ let id, aux = invent_name aux univ in
+ let univ = Option.get (Level.name univ) in
+ aux, (id,univ) :: univs)
+ (LSet.diff levels named) ((pl,0),univs)
in
- Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
+ input_univ_names (QualifiedUniv l, univs)
let do_universe ~poly l =
let in_section = Global.sections_are_opened () in
@@ -104,7 +138,7 @@ let do_universe ~poly l =
Univ.LSet.empty l, Univ.Constraint.empty
in
let src = if poly then BoundUniv else UnqualifiedUniv in
- let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
+ let () = input_univ_names (src, l) in
DeclareUctx.declare_universe_context ~poly ctx
let do_constraint ~poly l =
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index ca990a58eb..a7e942be5a 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -10,11 +10,16 @@
open Names
-(* object_kind , id *)
+(** Also used by [Declare] for constants, [DeclareInd] for inductives, etc.
+ Containts [object_kind , id]. *)
exception AlreadyDeclared of (string option * Id.t)
-(** Global universe contexts, names and constraints *)
+(** Internally used to declare names of universes from monomorphic
+ constants/inductives. Noop on polymorphic references. *)
val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
+(** Command [Universes]. *)
val do_universe : poly:bool -> lident list -> unit
+
+(** Command [Constraint]. *)
val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d35e13c4ef..bff0359782 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1325,14 +1325,28 @@ let decline_string n s =
else if Int.equal n 1 then str "1 " ++ str s
else (int n ++ str " " ++ str s ++ str "s")
-let explain_wrong_numarg_constructor env cstr n =
- str "The constructor " ++ pr_constructor env cstr ++
- str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
- str ") expects " ++ decline_string n "argument" ++ str "."
-
-let explain_wrong_numarg_inductive env ind n =
- str "The inductive type " ++ pr_inductive env ind ++
- str " expects " ++ decline_string n "argument" ++ str "."
+let explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp =
+ (if expanded then
+ strbrk "Once notations are expanded, the resulting "
+ else
+ strbrk "The ") ++ pp ++
+ strbrk " is expected to be applied to " ++ decline_string expected_nassums "argument" ++
+ (if expected_nassums = expected_ndecls then mt () else
+ strbrk " (or " ++ decline_string expected_ndecls "argument" ++
+ strbrk " when including variables for local definitions)") ++
+ strbrk " while it is actually applied to " ++
+ decline_string nargs "argument" ++ str "."
+
+let explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls =
+ let pp =
+ strbrk "constructor " ++ pr_constructor env cstr ++
+ strbrk " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
+ strbrk ")" in
+ explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
+
+let explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls =
+ let pp = strbrk "inductive type " ++ pr_inductive env ind in
+ explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
let explain_unused_clause env pats =
str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
@@ -1357,10 +1371,10 @@ let explain_pattern_matching_error env sigma = function
explain_bad_pattern env sigma c t
| BadConstructor (c,ind) ->
explain_bad_constructor env c ind
- | WrongNumargConstructor (c,n) ->
- explain_wrong_numarg_constructor env c n
- | WrongNumargInductive (c,n) ->
- explain_wrong_numarg_inductive env c n
+ | WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls} ->
+ explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls
+ | WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls} ->
+ explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls
| UnusedClause tms ->
explain_unused_clause env tms
| NonExhaustive tms ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 06eb330958..2fe402ff08 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1793,15 +1793,9 @@ let remove_delimiters local scope =
let add_class_scope local scope cl =
Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
-(* Check if abbreviation to a name and avoid early insertion of
- maximal implicit arguments *)
-let try_interp_name_alias = function
- | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
- | _ -> raise Not_found
-
let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
let acvars,pat,reversibility =
- try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
+ try Id.Map.empty, try_interp_name_alias (vars,c), APrioriReversible
with Not_found ->
let fold accu id = Id.Map.add id NtnInternTypeAny accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
@@ -1822,9 +1816,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
(* Declaration of custom entry *)
let warn_custom_entry =
- CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing"
+ CWarnings.create ~name:"custom-entry-overridden" ~category:"parsing"
(fun s ->
- strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.")
+ strbrk "Custom entry " ++ str s ++ strbrk " has been overridden.")
let load_custom_entry _ _ = ()
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 0fc6c7f87b..79a0cdf8d1 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -947,7 +947,7 @@ let print_about_any ?loc env sigma k udecl =
[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
| Syntactic kn ->
let () = match Syntax_def.search_syntactic_definition kn with
- | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
+ | [],Notation_term.NRef (ref,_) -> Dumpglob.add_glob ?loc ref
| _ -> () in
v 0 (
print_syntactic_def env kn ++ fnl () ++
diff --git a/vernac/record.ml b/vernac/record.ml
index 583164a524..96e4a47d2d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -366,7 +366,7 @@ let build_named_proj ~primitive ~flags ~poly ~univs ~uinstance ~kind env paramde
let ci = Inductiveops.make_case_info env indsp rci LetStyle in
(* Record projections are always NoInvert because they're at
constant relevance *)
- mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+ mkCase (Inductive.contract_case env (ci, p, NoInvert, mkRel 1, [|branch|])), None
in
let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
@@ -625,7 +625,7 @@ let build_class_constant ~univs ~rdata field implfs params paramimpls coers bind
let cref = GlobRef.ConstRef cst in
Impargs.declare_manual_implicits false cref paramimpls;
Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd implfs);
- Classes.set_typeclass_transparency (EvalConstRef cst) false false;
+ Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false;
let sub = List.hd coers in
let m = {
meth_name = Name proj_name;
@@ -744,7 +744,7 @@ let add_constant_class env sigma cst =
}
in
Classes.add_class env sigma tc;
- Classes.set_typeclass_transparency (EvalConstRef cst) false false
+ Classes.set_typeclass_transparency (Tacred.EvalConstRef cst) false false
let add_inductive_class env sigma ind =
let mind, oneind = Inductive.lookup_mind_specif env ind in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a3726daf63..4f3fc46c12 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -309,6 +309,17 @@ let print_registered () =
in
hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
+let dump_universes output g =
+ let open Univ in
+ let dump_arc u = function
+ | UGraph.Node ltle ->
+ Univ.LMap.iter (fun v strict ->
+ let typ = if strict then Lt else Le in
+ output typ u v) ltle;
+ | UGraph.Alias v ->
+ output Eq u v
+ in
+ Univ.LMap.iter dump_arc g
let dump_universes_gen prl g s =
let output = open_out s in
@@ -342,7 +353,7 @@ let dump_universes_gen prl g s =
in
let output_constraint k l r = output_constraint k (prl l) (prl r) in
try
- UGraph.dump_universes output_constraint g;
+ dump_universes output_constraint g;
close ();
str "Universes written to file \"" ++ str s ++ str "\"."
with reraise ->
@@ -367,13 +378,66 @@ let universe_subgraph ?loc kept univ =
let univ = LSet.fold add kept UGraph.initial_universes in
UGraph.merge_constraints csts univ
+let sort_universes g =
+ let open Univ in
+ let rec normalize u = match LMap.find u g with
+ | UGraph.Alias u -> normalize u
+ | UGraph.Node _ -> u
+ in
+ let get_next u = match LMap.find u g with
+ | UGraph.Alias u -> assert false (* nodes are normalized *)
+ | UGraph.Node ltle -> ltle
+ in
+ (* Compute the longest chain of Lt constraints from Set to any universe *)
+ let rec traverse accu todo = match todo with
+ | [] -> accu
+ | (u, n) :: todo ->
+ let () = assert (Level.equal (normalize u) u) in
+ let n = match LMap.find u accu with
+ | m -> if m < n then Some n else None
+ | exception Not_found -> Some n
+ in
+ match n with
+ | None -> traverse accu todo
+ | Some n ->
+ let accu = LMap.add u n accu in
+ let next = get_next u in
+ let fold v lt todo =
+ let v = normalize v in
+ if lt then (v, n + 1) :: todo else (v, n) :: todo
+ in
+ let todo = LMap.fold fold next todo in
+ traverse accu todo
+ in
+ (* Only contains normalized nodes *)
+ let levels = traverse LMap.empty [normalize Level.set, 0] in
+ let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in
+ let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in
+ let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in
+ let ulevels = Array.cons Level.set ulevels in
+ (* Add the normal universes *)
+ let fold (cur, ans) u =
+ let ans = LMap.add cur (UGraph.Node (LMap.singleton u true)) ans in
+ (u, ans)
+ in
+ let _, ans = Array.fold_left fold (Level.prop, LMap.empty) ulevels in
+ (* Add alias pointers *)
+ let fold u _ ans =
+ if Level.is_small u then ans
+ else
+ let n = LMap.find (normalize u) levels in
+ LMap.add u (UGraph.Alias ulevels.(n)) ans
+ in
+ LMap.fold fold g ans
+
let print_universes ?loc ~sort ~subgraph dst =
let univ = Global.universes () in
let univ = match subgraph with
| None -> univ
| Some g -> universe_subgraph ?loc g univ
in
- let univ = if sort then UGraph.sort_universes univ else univ in
+ let univ = UGraph.repr univ in
+ let univ = if sort then sort_universes univ else univ in
let pr_remaining =
if Global.is_joined_environment () then mt ()
else str"There may remain asynchronous universe constraints"
@@ -1628,6 +1692,7 @@ let () =
}
let vernac_set_strategy ~local l =
+ let open Tacred in
let local = Option.default false local in
let glob_ref r =
match smart_global r with
@@ -1639,6 +1704,7 @@ let vernac_set_strategy ~local l =
Redexpr.set_strategy local l
let vernac_set_opacity ~local (v,l) =
+ let open Tacred in
let local = Option.default true local in
let glob_ref r =
match smart_global r with
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:48:49 +0000