From 13ce46be7393ff304280c0701cf2b71299bbfbd8 Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Tue, 10 Mar 2026 19:32:21 +0100 Subject: [PATCH] Fix instance argument to Print and About with sort_variables --- doc/sphinx/proof-engine/vernacular-commands.rst | 2 +- doc/tools/docgram/fullGrammar | 2 +- doc/tools/docgram/orderedGrammar | 2 +- engine/univNames.ml | 4 +--- engine/univNames.mli | 4 +--- printing/printer.mli | 2 +- vernac/g_vernac.mlg | 2 +- vernac/prettyp.mli | 4 ++-- vernac/printmod.mli | 2 +- vernac/vernacexpr.mli | 4 ++-- 10 files changed, 12 insertions(+), 16 deletions(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1a98906234a7..e61401feab48 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -16,7 +16,7 @@ Displaying .. insertprodn univ_name_list univ_name_list .. prodn:: - univ_name_list ::= @%{ {* @name } %} + univ_name_list ::= @%{ {* @name } {? ; {* @name } } %} Displays definitions of terms, including opaque terms, for the object :n:`@reference`. diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 7016896cae35..b8017b485a5d 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1566,7 +1566,7 @@ search_queries: [ ] univ_name_list: [ -| "@{" LIST0 name "}" +| "@{" LIST0 name OPT [ ";" LIST0 name ] "}" ] syntax: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5fa00c28c5ef..2e7466bc2702 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1096,7 +1096,7 @@ logical_kind: [ ] univ_name_list: [ -| "@{" LIST0 name "}" +| "@{" LIST0 name OPT [ ";" LIST0 name ] "}" ] enable_notation_flag: [ diff --git a/engine/univNames.ml b/engine/univNames.ml index 71e97ae8bc1e..2689cb1e1975 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -20,9 +20,7 @@ let empty_binders = Id.Map.empty, Id.Map.empty let empty_rev_binders = QVar.Map.empty, Level.Map.empty -type univ_name_list = Names.lname list - -type full_name_list = lname list * lname list +type univ_name_list = lname list * lname list let qualid_of_level (_,ctx) l = match Level.name l with diff --git a/engine/univNames.mli b/engine/univNames.mli index 9149a0d67c4d..80b04c0cd07a 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -22,9 +22,7 @@ val empty_binders : universe_binders val empty_rev_binders : rev_binders -type univ_name_list = Names.lname list - -type full_name_list = lname list * lname list +type univ_name_list = lname list * lname list val pr_level_with_global_universes : ?binders:universe_binders -> Level.t -> Pp.t val qualid_of_level : universe_binders -> Level.t -> Libnames.qualid option diff --git a/printing/printer.mli b/printing/printer.mli index 7925a1a286ec..e88e6caba771 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -163,7 +163,7 @@ val pr_universes : evar_map -> Inefficient on large contexts due to name generation. *) val universe_binders_with_opt_names : UVars.AbstractContext.t -> - (GlobRef.t * UnivNames.full_name_list) option -> UnivNames.universe_binders * UnivNames.rev_binders + (GlobRef.t * UnivNames.univ_name_list) option -> UnivNames.universe_binders * UnivNames.rev_binders (** Printing global references using names as short as possible *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 030a62269d33..5a5189fb8253 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1327,7 +1327,7 @@ GRAMMAR EXTEND Gram ] ] ; univ_name_list: - [ [ "@{" ; l = LIST0 name; "}" -> { [],l } ] ] + [ [ "@{" ; l = LIST0 name; l' = OPT [ ";" ; l = LIST0 name -> { l } ] ; "}" -> { match l' with None -> [], l | Some l' -> l, l' } ] ] ; END diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index 0ae97edbca35..06cb12b2a199 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -41,7 +41,7 @@ val print_safe_judgment : Safe_typing.judgment -> Pp.t val print_name : Global.indirect_accessor -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.full_name_list option + -> UnivNames.univ_name_list option -> Pp.t val print_notation : env -> Evd.evar_map -> qualid Constrexpr.notation_entry_gen @@ -51,7 +51,7 @@ val print_notation : env -> Evd.evar_map val print_abbreviation : Global.indirect_accessor -> env -> Evd.evar_map -> KerName.t -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.full_name_list option -> Pp.t + UnivNames.univ_name_list option -> Pp.t val print_impargs : env -> GlobRef.t -> Pp.t (** Pretty-printing functions for classes and coercions *) diff --git a/vernac/printmod.mli b/vernac/printmod.mli index 706e7d5b8af4..d53593366292 100644 --- a/vernac/printmod.mli +++ b/vernac/printmod.mli @@ -12,6 +12,6 @@ open Names val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> - UnivNames.full_name_list option -> Pp.t + UnivNames.univ_name_list option -> Pp.t val print_module : with_body:bool -> ModPath.t -> Pp.t val print_modtype : ModPath.t -> Pp.t diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli index 5ac95d8bcedf..f1d6e80d11ab 100644 --- a/vernac/vernacexpr.mli +++ b/vernac/vernacexpr.mli @@ -53,7 +53,7 @@ type printable = | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of qualid or_by_notation * UnivNames.full_name_list option + | PrintName of qualid or_by_notation * UnivNames.univ_name_list option | PrintGraph | PrintClasses | PrintTypeclasses @@ -70,7 +70,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of qualid or_by_notation * UnivNames.full_name_list option * Goal_select.t option + | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option | PrintImplicit of qualid or_by_notation | PrintAssumptions of bool * bool * qualid or_by_notation list | PrintStrategy of qualid or_by_notation option