Skip to content

Fix instance argument to Print and About with sort variables #21738

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 1 commit into from
Mar 12, 2026
+12 −16
Merged

Fix instance argument to Print and About with sort variables #21738

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion doc/sphinx/proof-engine/vernacular-commands.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

Expand Down
2 changes: 1 addition & 1 deletion doc/tools/docgram/fullGrammar
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1566,7 +1566,7 @@ search_queries: [
]

univ_name_list: [
| "@{" LIST0 name "}"
| "@{" LIST0 name OPT [ ";" LIST0 name ] "}"
]

syntax: [
Expand Down
2 changes: 1 addition & 1 deletion doc/tools/docgram/orderedGrammar
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1096,7 +1096,7 @@ logical_kind: [
]

univ_name_list: [
| "@{" LIST0 name "}"
| "@{" LIST0 name OPT [ ";" LIST0 name ] "}"
]

enable_notation_flag: [
Expand Down
4 changes: 1 addition & 3 deletions engine/univNames.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 1 addition & 3 deletions engine/univNames.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion printing/printer.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)

Expand Down
2 changes: 1 addition & 1 deletion vernac/g_vernac.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 2 additions & 2 deletions vernac/prettyp.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 *)
Expand Down
2 changes: 1 addition & 1 deletion vernac/printmod.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 2 additions & 2 deletions vernac/vernacexpr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down