From e6a2fb9b2fa240194e1469439b56339b9b415d78 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 10 Feb 2026 10:11:15 +0100 Subject: [PATCH 1/2] Add "of _ & _ & _" syntax for constructors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit e.g.: Variant t := C1 of a & b & c | C2 x y of P x & Q y. Co-authored-by: Gaëtan Gilbert --- .../02-specification-language/21611-of-ampersand.rst | 7 +++++++ doc/sphinx/language/core/basic.rst | 2 +- doc/sphinx/language/core/inductive.rst | 5 ++++- doc/tools/docgram/common.edit_mlg | 5 +++-- doc/tools/docgram/fullGrammar | 6 +++++- doc/tools/docgram/orderedGrammar | 2 +- test-suite/output/PrintKeywords.out | 1 + theories/Corelib/Classes/CMorphisms.v | 2 +- theories/Corelib/Classes/Morphisms.v | 2 +- vernac/g_vernac.mlg | 12 ++++++++++-- 10 files changed, 34 insertions(+), 10 deletions(-) create mode 100644 doc/changelog/02-specification-language/21611-of-ampersand.rst diff --git a/doc/changelog/02-specification-language/21611-of-ampersand.rst b/doc/changelog/02-specification-language/21611-of-ampersand.rst new file mode 100644 index 000000000000..47679970f648 --- /dev/null +++ b/doc/changelog/02-specification-language/21611-of-ampersand.rst @@ -0,0 +1,7 @@ +- **Added:** + new syntactic sugars `of T & ... & T` for anonymous binders + `(_ : T)` in constructors, enabling the + `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax. + This adds the new reserved keyword `of` + (`#21611 `_, + by Pierre Roux). diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9500325363e9..f0a5a7666947 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -189,7 +189,7 @@ Keywords _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop SProp Set Theorem Type Variable as at cofix else end - fix for forall fun if in let match return then where with + fix for forall fun if in let match of return then where with The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 7b68a55e6ed9..00bca1b0b1ae 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,7 +32,7 @@ Inductive types .. prodn:: inductive_definition ::= @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } := {? {? %| } {+| @constructor } } {? @decl_notations } - constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? @of_type_inst } + constructor ::= {* #[ {+, @attribute } ] } @ident {* @binder } {? of {+& @term99 } } {? @of_type_inst } Defines one or more inductive types and its constructors. Rocq generates @@ -100,6 +100,9 @@ Inductive types Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case the actual type of the constructor is :n:`forall {* @binder }, @type`. + :n:`{? of {+& @term99 } }` + `of T1 & ... & Tn` is syntactic sugar for anonymous binders `(_ : T1) ... (_ : Tn)`. + .. exn:: Non strictly positive occurrence of @ident in @type. The types of the constructors have to satisfy a *positivity diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 2b12707243fe..cf70461c9093 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1457,8 +1457,8 @@ assumpt: [ ] constructor_type: [ -| REPLACE binders [ of_type_inst lconstr | ] -| WITH binders OPT of_type_inst +| REPLACE constructor_binders [ of_type_inst lconstr | ] +| WITH constructor_binders OPT of_type_inst ] (* todo: is this really correct? Search for "Pvernac.register_proof_mode" *) @@ -2299,6 +2299,7 @@ SPLICE: [ | preident | lpar_id_coloneq | binders +| constructor_binders | check_module_types | decl_sep | function_fix_definition (* loses funind annotation *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index ffd5402734a2..747ccfd2dc2a 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1135,8 +1135,12 @@ assumpt: [ | LIST1 ident_decl of_type lconstr ] +constructor_binders: [ +| binders OPT [ "of" LIST1 term99 SEP "&" ] +] + constructor_type: [ -| binders [ of_type_inst lconstr | ] +| constructor_binders [ of_type_inst lconstr | ] ] constructor: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d3cd93739132..09d7959b3ae0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -572,7 +572,7 @@ inductive_definition: [ ] constructor: [ -| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT of_type_inst +| LIST0 [ "#[" LIST1 attribute SEP "," "]" ] ident LIST0 binder OPT [ "of" LIST1 term99 SEP "&" ] OPT of_type_inst ] import_categories: [ diff --git a/test-suite/output/PrintKeywords.out b/test-suite/output/PrintKeywords.out index f25f491e162f..7dc6175218a7 100644 --- a/test-suite/output/PrintKeywords.out +++ b/test-suite/output/PrintKeywords.out @@ -83,6 +83,7 @@ if in let match +of return then using diff --git a/theories/Corelib/Classes/CMorphisms.v b/theories/Corelib/Classes/CMorphisms.v index 54ad5fbdd091..59fd8f59ab6b 100644 --- a/theories/Corelib/Classes/CMorphisms.v +++ b/theories/Corelib/Classes/CMorphisms.v @@ -437,7 +437,7 @@ Section GenericInstances. Proper R' (m x). Proof. simpl_crelation. Qed. - Class Params {A} (of : A) (arity : nat). + Class Params {A} (from : A) (arity : nat). Lemma flip_respectful {A B} (R : crelation A) (R' : crelation B) : relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). diff --git a/theories/Corelib/Classes/Morphisms.v b/theories/Corelib/Classes/Morphisms.v index 79b24b3dff00..19a94ca3c88e 100644 --- a/theories/Corelib/Classes/Morphisms.v +++ b/theories/Corelib/Classes/Morphisms.v @@ -538,7 +538,7 @@ Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. -Class Params {A : Type} (of : A) (arity : nat). +Class Params {A : Type} (from : A) (arity : nat). #[global] Instance eq_pars : Params (@eq) 1 := {}. #[global] Instance iff_pars : Params (@iff) 0 := {}. #[global] Instance impl_pars : Params (@impl) 0 := {}. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index f8c59c08a039..030a62269d33 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -639,9 +639,17 @@ GRAMMAR EXTEND Gram { (oc,(idl,c)) } ] ] ; + constructor_binders: + [ [ l1 = binders; l2 = OPT [ "of"; l = LIST1 term LEVEL "99" SEP "&" -> { l } ] -> + { let anon c = + let n = CAst.make ?loc:c.CAst.loc Anonymous in + CLocalAssum ([n], None, Default Explicit, c) in + l1 @ List.map anon (Option.default [] l2) } ] ] + ; + constructor_type: - [[ l = binders; - t= [ coe = of_type_inst; c = lconstr -> + [[ l = constructor_binders; + t = [ coe = of_type_inst; c = lconstr -> { fun l attr id -> ((attr, fst coe, snd coe),(id,mkProdCN ~loc l c)) } | -> { fun l attr id -> ((attr,NoCoercion,NoInstance),(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None)))) } ] From af52fac7294bdc9253eec85f8cbc8622bd7894e4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 17 Feb 2026 11:15:33 +0100 Subject: [PATCH 2/2] Add `& T` syntax for anonymous binders `(_ : T)` --- .../02-specification-language/21611-of-ampersand.rst | 4 ++-- .../07-ssreflect/21611-of-ampersand-of-Removed.rst | 5 +++++ doc/sphinx/language/core/assumptions.rst | 3 +++ doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + parsing/g_constr.mlg | 4 +++- plugins/ssr/ssrvernac.mlg | 8 -------- test-suite/prerequisite/ssr_mini_mathcomp.v | 6 +++--- theories/Corelib/ssr/ssreflect.v | 2 +- 9 files changed, 19 insertions(+), 15 deletions(-) create mode 100644 doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst diff --git a/doc/changelog/02-specification-language/21611-of-ampersand.rst b/doc/changelog/02-specification-language/21611-of-ampersand.rst index 47679970f648..0f086e21b45d 100644 --- a/doc/changelog/02-specification-language/21611-of-ampersand.rst +++ b/doc/changelog/02-specification-language/21611-of-ampersand.rst @@ -1,6 +1,6 @@ - **Added:** - new syntactic sugars `of T & ... & T` for anonymous binders - `(_ : T)` in constructors, enabling the + new syntactic sugars `& T` for anonymous binders `(_ : T)` + and `of T & ... & T` for anonymous binders in constructors, enabling the `Variant t := C1 of a & b & c | C2 x y of P x & Q y.` syntax. This adds the new reserved keyword `of` (`#21611 `_, diff --git a/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst b/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst new file mode 100644 index 000000000000..c2b0d6113d31 --- /dev/null +++ b/doc/changelog/07-ssreflect/21611-of-ampersand-of-Removed.rst @@ -0,0 +1,5 @@ +- **Removed:** + the `of T` syntax for anonymous binders outside of constructors, + use `& T` instead + (`#21611 `_, + by Pierre Roux). diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 87d599895a91..da88b5a039b8 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -20,6 +20,7 @@ Binders | @generalizing_binder | ( @name : @type %| @term ) | ' @pattern0 + | & @term99 Various constructions such as :g:`fun`, :g:`forall`, :g:`fix` and :g:`cofix` *bind* variables. A binding is represented by an identifier. If the binding @@ -38,6 +39,8 @@ variable can be introduced at the same time. It is also possible to give the type of the variable as follows: :n:`(@ident : @type := @term)`. +:n:`& @term99` is syntactic sugar for the anonymous binder :n:`(_ : @term99)`. + `(x : T | P)` is syntactic sugar for `(x : @Corelib.Init.Specif.sig _ (fun x : T => P))`, which would more typically be written `(x : {x : T | P})`. Since `(x : T | P)` uses `sig` directly, diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 747ccfd2dc2a..36cff2190314 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -348,6 +348,7 @@ closed_binder: [ | "`{" LIST1 typeclass_constraint SEP "," "}" | "`[" LIST1 typeclass_constraint SEP "," "]" | "'" pattern0 +| "&" term99 ] one_open_binder: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 09d7959b3ae0..f2b81f604e1d 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -405,6 +405,7 @@ binder: [ | generalizing_binder | "(" name ":" type "|" term ")" | "'" pattern0 +| "&" term99 ] implicit_binders: [ diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 4261636d27d8..00fcb117a02f 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -508,7 +508,9 @@ GRAMMAR EXTEND Gram { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (MaxImplicit, b), t)) tc } | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" -> { List.map (fun (n, b, t) -> CLocalAssum ([n], None, Generalized (NonMaxImplicit, b), t)) tc } - | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } ] ] + | "'"; p = pattern LEVEL "0" -> { [CLocalPattern p] } + | "&"; c = term LEVEL "99" -> + { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] } ] ] ; one_open_binder: [ [ na = name -> { (pat_of_name na, Explicit) } diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 1df591df336e..d93101b33c13 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -116,14 +116,6 @@ GRAMMAR EXTEND Gram ] ]; END -GRAMMAR EXTEND Gram - GLOBAL: closed_binder; - closed_binder: TOP [ - [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> - { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] } - ] ]; -END - (** Vernacular commands: Prenex Implicits *) (* This should really be implemented as an extension to the implicit *) diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 083e9681269c..78a41c2501ef 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -695,7 +695,7 @@ Structure type := Pack {sort; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. +Definition clone c & phant_id class c := @Pack T c T. Let xT := let: Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). @@ -798,7 +798,7 @@ Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. +Definition clone c & phant_id class c := @Pack T c T. Let xT := let: Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). @@ -948,7 +948,7 @@ Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}. Local Coercion sort : type >-> Sortclass. Variables (T : Type) (cT : type). Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. +Definition clone c & phant_id class c := @Pack T c T. Let xT := let: Pack T _ _ := cT in T. Notation xclass := (class : class_of xT). diff --git a/theories/Corelib/ssr/ssreflect.v b/theories/Corelib/ssr/ssreflect.v index 458d179955a3..ee59e60a7753 100644 --- a/theories/Corelib/ssr/ssreflect.v +++ b/theories/Corelib/ssr/ssreflect.v @@ -231,7 +231,7 @@ Variant put vT sT (v1 v2 : vT) (s : sT) : Prop := Put. Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s. -Definition get_by vT sT of sT -> vT := @get vT sT. +Definition get_by vT sT & sT -> vT := @get vT sT. End TheCanonical.