Skip to content

Commit 0cfe513

Browse files
SkySkimmerSkySkimmer
committed
Revert name change of univ_decl to sort_poly_decl
1 parent ccced7c commit 0cfe513

39 files changed

+345
-347
lines changed

‎doc/sphinx/addendum/rewrite-rules.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@ Rewrite rules
4949
.. insertprodn rewrite_rule rewrite_rule
5050
5151
.. prodn::
52-
rewrite_rule ::= {? @sort_poly_decl %|- } @rw_pattern => @term
52+
rewrite_rule ::= {? @univ_decl %|- } @rw_pattern => @term
5353

5454
Declares a named block of rewrite rules. The name is declared in the same namespace as constants and inductives.
5555

‎doc/sphinx/addendum/universe-polymorphism.rst‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -524,7 +524,7 @@ it is an atomic universe (i.e. not an algebraic max() universe).
524524
Explicit Universes
525525
-------------------
526526

527-
.. insertprodn universe_name sort_poly_constraint
527+
.. insertprodn universe_name sort_constraint
528528
529529
.. prodn::
530530
universe_name ::= @qualid
@@ -542,9 +542,9 @@ Explicit Universes
542542
| SProp
543543
| Type
544544
| @qualid
545-
sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
546-
cumul_sort_poly_decl ::= @%{ {? {* @ident } {| %| | ; } } {* {? {| + | = | * } } @ident } {? + } {? %| {*, @sort_poly_constraint } {? + } } %}
547-
sort_poly_constraint ::= @universe_name {| < | = | <= } @universe_name
545+
univ_decl ::= @%{ {? {* @ident } {| %| | ; } } {* @ident } {? + } {? %| {*, @sort_constraint } {? + } } %}
546+
cumul_univ_decl ::= @%{ {? {* @ident } {| %| | ; } } {* {? {| + | = | * } } @ident } {? + } {? %| {*, @sort_constraint } {? + } } %}
547+
sort_constraint ::= @universe_name {| < | = | <= } @universe_name
548548
| @sort_quality_var -> @sort_quality_var
549549
550550
The syntax has been extended to allow users to explicitly bind names
@@ -563,7 +563,7 @@ to universes and explicitly instantiate polymorphic definitions.
563563
.. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead.
564564
:undocumented:
565565

566-
.. cmd:: Constraint {+, @sort_poly_constraint }
566+
.. cmd:: Constraint {+, @sort_constraint }
567567

568568
Declares new constraints between named universes.
569569

@@ -814,7 +814,7 @@ All sort quality variables must be explicitly bound.
814814

815815
Polymorphic Definition sort'@{s | u |} := Type@{s|u}.
816816
817-
To help the parser, both `|` in the :n:`@sort_poly_decl` are required.
817+
To help the parser, both `|` in the :n:`@univ_decl` are required.
818818

819819
Sort quality variables of a sort polymorphic definition may be
820820
instantiated by the concrete values `SProp`, `Prop` and `Type` or by a

‎doc/sphinx/language/core/assumptions.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -171,7 +171,7 @@ has type :n:`@type`.
171171
| {| Hypothesis | Hypotheses }
172172
| {| Variable | Variables }
173173
assumpt ::= {+ @ident_decl } @of_type
174-
ident_decl ::= @ident {? @sort_poly_decl }
174+
ident_decl ::= @ident {? @univ_decl }
175175
of_type ::= {| : | :> } @type
176176

177177
These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in

‎doc/sphinx/language/core/inductive.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ Inductive types
3131
.. insertprodn inductive_definition constructor
3232
3333
.. prodn::
34-
inductive_definition ::= @ident {? @cumul_sort_poly_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
34+
inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations }
3535
constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? @of_type_inst }
3636

3737
Defines one or more

‎doc/sphinx/language/core/modules.rst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ together, as well as a means of massive abstraction.
7373
| ( @module_type )
7474
| @module_type @module_expr_atom
7575
| @module_type with @with_declaration
76-
with_declaration ::= Definition @qualid {? @sort_poly_decl } := @term
76+
with_declaration ::= Definition @qualid {? @univ_decl } := @term
7777
| Module @qualid := @qualid
7878
module_expr_atom ::= @qualid
7979
| ( @module_expr_atom )

‎doc/tools/docgram/common.edit_mlg‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -171,9 +171,9 @@ DELETE: [
171171
| test_old_sort_qvar
172172
| test_sort_qvar
173173
| test_ltac2_ident
174-
| test_doublepipe_sort_poly_decl
175-
| test_doublepipe_cumul_sort_poly_decl
176-
| test_semicolon_cumul_sort_poly_decl
174+
| test_doublepipe_univ_decl
175+
| test_doublepipe_cumul_univ_decl
176+
| test_semicolon_cumul_univ_decl
177177
| test_univ_cst
178178
]
179179

@@ -648,18 +648,18 @@ univ_level_or_quality: [
648648
| WITH "0"
649649
]
650650

651-
sort_poly_decl: [
652-
| REPLACE "@{" LIST0 identref ";" LIST0 identref [ "+" | ] sort_poly_decl_constraints
653-
| WITH "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 identref OPT "+" OPT [ "|" LIST0 sort_poly_constraint SEP "," OPT "+" ] "}"
654-
| DELETE "@{" LIST0 identref [ "+" | ] sort_poly_decl_constraints
655-
| DELETE "@{" LIST0 identref "|" LIST0 identref [ "+" | ] sort_poly_decl_constraints
651+
univ_decl: [
652+
| REPLACE "@{" LIST0 identref ";" LIST0 identref [ "+" | ] univ_decl_constraints
653+
| WITH "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 identref OPT "+" OPT [ "|" LIST0 sort_constraint SEP "," OPT "+" ] "}"
654+
| DELETE "@{" LIST0 identref [ "+" | ] univ_decl_constraints
655+
| DELETE "@{" LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
656656
]
657657

658-
cumul_sort_poly_decl: [
659-
| REPLACE "@{" LIST0 identref ";" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
660-
| WITH "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 variance_identref OPT "+" OPT [ "|" LIST0 sort_poly_constraint SEP "," OPT "+" ] "}"
661-
| DELETE "@{" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
662-
| DELETE "@{" LIST0 identref "|" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
658+
cumul_univ_decl: [
659+
| REPLACE "@{" LIST0 identref ";" LIST0 variance_identref [ "+" | ] univ_decl_constraints
660+
| WITH "@{" OPT [ LIST0 identref [ "|" | ";" ] ] LIST0 variance_identref OPT "+" OPT [ "|" LIST0 sort_constraint SEP "," OPT "+" ] "}"
661+
| DELETE "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
662+
| DELETE "@{" LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
663663
]
664664

665665
of_type: [
@@ -734,9 +734,9 @@ gallina_ext: [
734734

735735
(* Per @Zimmi48, the global (qualid) must be a simple identifier if def_body is present
736736
Note that smart_global is "qualid | by_notation" and that
737-
ident_decl is "ident OPT sort_poly_decl"; move
737+
ident_decl is "ident OPT univ_decl"; move
738738
*)
739-
| REPLACE "Canonical" OPT "Structure" global OPT [ OPT sort_poly_decl def_body ]
739+
| REPLACE "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
740740
| WITH "Canonical" OPT "Structure" ident_decl def_body
741741
| REPLACE "Canonical" OPT "Structure" by_notation
742742
| WITH "Canonical" OPT "Structure" smart_global
@@ -746,8 +746,8 @@ gallina_ext: [
746746
| WITH "Coercion" smart_global OPT [ ":" coercion_class ">->" coercion_class ]
747747

748748
(* semantically restricted per https://github.com/rocq-prover/rocq/pull/12936#discussion_r492705820 *)
749-
(* global OPT sort_poly_decl is just ident_decl, the first OPT is moved to the rule above *)
750-
| REPLACE "Coercion" global OPT [ OPT sort_poly_decl def_body ]
749+
(* global OPT univ_decl is just ident_decl, the first OPT is moved to the rule above *)
750+
| REPLACE "Coercion" global OPT [ OPT univ_decl def_body ]
751751
| WITH "Coercion" ident_decl def_body
752752

753753
| REPLACE "Include" "Type" module_type_inl LIST0 ext_module_type

‎doc/tools/docgram/fullGrammar‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -918,7 +918,7 @@ gallina: [
918918
| "Universes" LIST1 identref
919919
| "Sort" LIST1 identref
920920
| "Sorts" LIST1 identref
921-
| "Constraint" LIST1 sort_poly_constraint SEP ","
921+
| "Constraint" LIST1 sort_constraint SEP ","
922922
| "Rewrite" "Rule" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
923923
| "Rewrite" "Rules" identref ":=" OPT "|" LIST1 rewrite_rule SEP "|"
924924
]
@@ -965,20 +965,20 @@ inline: [
965965
|
966966
]
967967

968-
sort_poly_constraint: [
968+
sort_constraint: [
969969
| test_univ_cst universe_name [ "<" | "=" | "<=" ] universe_name
970970
| sort_quality_var "->" sort_quality_var
971971
]
972972

973-
sort_poly_decl_constraints: [
974-
| "|" LIST0 sort_poly_constraint SEP "," [ "+" | ] "}"
973+
univ_decl_constraints: [
974+
| "|" LIST0 sort_constraint SEP "," [ "+" | ] "}"
975975
| [ "}" | bar_cbrace ]
976976
]
977977

978-
sort_poly_decl: [
979-
| "@{" test_doublepipe_sort_poly_decl LIST0 identref "|" LIST0 identref [ "+" | ] sort_poly_decl_constraints
980-
| "@{" LIST0 identref ";" LIST0 identref [ "+" | ] sort_poly_decl_constraints
981-
| "@{" LIST0 identref [ "+" | ] sort_poly_decl_constraints
978+
univ_decl: [
979+
| "@{" test_doublepipe_univ_decl LIST0 identref "|" LIST0 identref [ "+" | ] univ_decl_constraints
980+
| "@{" LIST0 identref ";" LIST0 identref [ "+" | ] univ_decl_constraints
981+
| "@{" LIST0 identref [ "+" | ] univ_decl_constraints
982982
]
983983

984984
variance: [
@@ -992,18 +992,18 @@ variance_identref: [
992992
| test_variance_ident variance identref
993993
]
994994

995-
cumul_sort_poly_decl: [
996-
| "@{" test_doublepipe_cumul_sort_poly_decl LIST0 identref "|" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
997-
| "@{" test_semicolon_cumul_sort_poly_decl LIST0 identref ";" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
998-
| "@{" LIST0 variance_identref [ "+" | ] sort_poly_decl_constraints
995+
cumul_univ_decl: [
996+
| "@{" test_doublepipe_cumul_univ_decl LIST0 identref "|" LIST0 variance_identref [ "+" | ] univ_decl_constraints
997+
| "@{" test_semicolon_cumul_univ_decl LIST0 identref ";" LIST0 variance_identref [ "+" | ] univ_decl_constraints
998+
| "@{" LIST0 variance_identref [ "+" | ] univ_decl_constraints
999999
]
10001000

10011001
ident_decl: [
1002-
| identref OPT sort_poly_decl
1002+
| identref OPT univ_decl
10031003
]
10041004

10051005
cumul_ident_decl: [
1006-
| identref OPT cumul_sort_poly_decl
1006+
| identref OPT cumul_univ_decl
10071007
]
10081008

10091009
inductive_token: [
@@ -1083,7 +1083,7 @@ rw_pattern: [
10831083
]
10841084

10851085
rewrite_rule: [
1086-
| OPT [ sort_poly_decl "|-" ] rw_pattern "=>" lconstr
1086+
| OPT [ univ_decl "|-" ] rw_pattern "=>" lconstr
10871087
]
10881088

10891089
scheme: [
@@ -1175,9 +1175,9 @@ gallina_ext: [
11751175
| "Transparent" OPT "!" LIST1 smart_global
11761176
| "Opaque" OPT "!" LIST1 smart_global
11771177
| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
1178-
| "Canonical" OPT "Structure" global OPT [ OPT sort_poly_decl def_body ]
1178+
| "Canonical" OPT "Structure" global OPT [ OPT univ_decl def_body ]
11791179
| "Canonical" OPT "Structure" by_notation
1180-
| "Coercion" global OPT [ OPT sort_poly_decl def_body ]
1180+
| "Coercion" global OPT [ OPT univ_decl def_body ]
11811181
| "Identity" "Coercion" identref ":" coercion_class ">->" coercion_class
11821182
| "Coercion" global ":" coercion_class ">->" coercion_class
11831183
| "Coercion" by_notation ":" coercion_class ">->" coercion_class
@@ -1275,7 +1275,7 @@ module_expr_atom: [
12751275
]
12761276

12771277
with_declaration: [
1278-
| "Definition" fullyqualid OPT sort_poly_decl ":=" Constr.lconstr
1278+
| "Definition" fullyqualid OPT univ_decl ":=" Constr.lconstr
12791279
| "Module" fullyqualid ":=" qualid
12801280
]
12811281

‎doc/tools/docgram/orderedGrammar‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ assumpt: [
108108
]
109109

110110
ident_decl: [
111-
| ident OPT sort_poly_decl
111+
| ident OPT univ_decl
112112
]
113113

114114
of_type: [
@@ -321,21 +321,21 @@ sort_quality_var: [
321321
| qualid
322322
]
323323

324-
sort_poly_decl: [
325-
| "@{" OPT [ LIST0 ident [ "|" | ";" ] ] LIST0 ident OPT "+" OPT [ "|" LIST0 sort_poly_constraint SEP "," OPT "+" ] "}"
324+
univ_decl: [
325+
| "@{" OPT [ LIST0 ident [ "|" | ";" ] ] LIST0 ident OPT "+" OPT [ "|" LIST0 sort_constraint SEP "," OPT "+" ] "}"
326326
]
327327

328-
cumul_sort_poly_decl: [
329-
| "@{" OPT [ LIST0 ident [ "|" | ";" ] ] LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 sort_poly_constraint SEP "," OPT "+" ] "}"
328+
cumul_univ_decl: [
329+
| "@{" OPT [ LIST0 ident [ "|" | ";" ] ] LIST0 ( OPT [ "+" | "=" | "*" ] ident ) OPT "+" OPT [ "|" LIST0 sort_constraint SEP "," OPT "+" ] "}"
330330
]
331331

332-
sort_poly_constraint: [
332+
sort_constraint: [
333333
| universe_name [ "<" | "=" | "<=" ] universe_name
334334
| sort_quality_var "->" sort_quality_var
335335
]
336336

337-
sort_poly_decl_constraints: [
338-
| "|" LIST0 sort_poly_constraint SEP "," [ "+" | ] "}"
337+
univ_decl_constraints: [
338+
| "|" LIST0 sort_constraint SEP "," [ "+" | ] "}"
339339
| [ "}" | "|}" ]
340340
]
341341

@@ -565,7 +565,7 @@ field_val: [
565565
]
566566

567567
inductive_definition: [
568-
| ident OPT cumul_sort_poly_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT [ OPT "|" LIST1 constructor SEP "|" ] OPT decl_notations
568+
| ident OPT cumul_univ_decl LIST0 binder OPT [ "|" LIST0 binder ] OPT [ ":" type ] ":=" OPT [ OPT "|" LIST1 constructor SEP "|" ] OPT decl_notations
569569
]
570570

571571
constructor: [
@@ -589,7 +589,7 @@ rw_pattern: [
589589
]
590590

591591
rewrite_rule: [
592-
| OPT [ sort_poly_decl "|-" ] rw_pattern "=>" term
592+
| OPT [ univ_decl "|-" ] rw_pattern "=>" term
593593
]
594594

595595
scheme_kind: [
@@ -640,7 +640,7 @@ module_type: [
640640
]
641641

642642
with_declaration: [
643-
| "Definition" qualid OPT sort_poly_decl ":=" term
643+
| "Definition" qualid OPT univ_decl ":=" term
644644
| "Module" qualid ":=" qualid
645645
]
646646

@@ -946,7 +946,7 @@ command: [
946946
| "Universes" LIST1 ident
947947
| "Sort" LIST1 ident
948948
| "Sorts" LIST1 ident
949-
| "Constraint" LIST1 sort_poly_constraint SEP ","
949+
| "Constraint" LIST1 sort_constraint SEP ","
950950
| "Rewrite" [ "Rule" | "Rules" ] ident ":=" OPT "|" LIST1 rewrite_rule SEP "|"
951951
| "CoInductive" inductive_definition LIST0 ( "with" inductive_definition )
952952
| "CoInductive" record_definition LIST0 ( "with" record_definition )

‎engine/evd.ml‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1029,13 +1029,13 @@ let to_universe_context evd = UState.context evd.universes
10291029

10301030
let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
10311031

1032-
let check_sort_poly_decl ~poly evd decl = UState.check_sort_poly_decl ~poly evd.universes decl
1032+
let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
10331033

1034-
let check_sort_poly_decl_early ~poly ~with_obls sigma udecl terms =
1034+
let check_univ_decl_early ~poly ~with_obls sigma udecl terms =
10351035
let () =
10361036
if with_obls && not poly &&
1037-
(not udecl.UState.sort_poly_decl_extensible_instance
1038-
|| not udecl.UState.sort_poly_decl_extensible_constraints)
1037+
(not udecl.UState.univdecl_extensible_instance
1038+
|| not udecl.UState.univdecl_extensible_constraints)
10391039
then
10401040
CErrors.user_err
10411041
Pp.(str "Non extensible universe declaration not supported \
@@ -1045,7 +1045,7 @@ let check_sort_poly_decl_early ~poly ~with_obls sigma udecl terms =
10451045
let uctx = ustate sigma in
10461046
let uctx = UState.collapse_sort_variables uctx in
10471047
let uctx = UState.restrict uctx vars in
1048-
ignore (UState.check_sort_poly_decl ~poly uctx udecl)
1048+
ignore (UState.check_univ_decl ~poly uctx udecl)
10491049

10501050
let restrict_universe_context evd vars =
10511051
{ evd with universes = UState.restrict evd.universes vars }

‎engine/evd.mli‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -630,11 +630,11 @@ val to_universe_context : evar_map -> UVars.UContext.t
630630

631631
val univ_entry : poly:bool -> evar_map -> UState.named_universes_entry
632632

633-
val check_sort_poly_decl : poly:bool -> evar_map -> UState.sort_poly_decl -> UState.named_universes_entry
633+
val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> UState.named_universes_entry
634634

635635
(** An early check of compatibility of the universe declaration before
636636
starting to build a declaration interactively *)
637-
val check_sort_poly_decl_early : poly:bool -> with_obls:bool -> evar_map -> UState.sort_poly_decl -> Constr.t list -> unit
637+
val check_univ_decl_early : poly:bool -> with_obls:bool -> evar_map -> UState.universe_decl -> Constr.t list -> unit
638638

639639
val merge_universe_context : evar_map -> UState.t -> evar_map
640640
val set_universe_context : evar_map -> UState.t -> evar_map

0 commit comments

Comments
 (0)