Add "of _ & _ & _" syntax

Author: proux01

doc/changelog/02-specification-language/21611-of-ampersand.rst

@@ -0,0 +1,7 @@
+- **Added:**
+  new syntactic sugars `of T` and `& T` for anonymous binders
+  `(_ : T)`. In particular, this enables the
+  `Variant t := C1 of a & b & c | C2 of d.` syntax.
+  This adds the new reserved keyword `of`
+  (`#21478 <https://github.com/rocq-prover/rocq/pull/21478>`_,
+  by Pierre Roux).

doc/sphinx/language/core/assumptions.rst

@@ -20,6 +20,7 @@ Binders
    | @generalizing_binder
    | ( @name : @type %| @term )
    | ' @pattern0
+   | {| of | & } @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)`.
 
+`of T` and `& T` are syntactic sugar for anonymous binders `(_ : T)`.
+
 `(x : T | P)` is syntactic sugar for `(x : @Stdlib.Init.Specif.sig _ (fun x : T => P))`,
 which would more typically be written `(x : {x : T | P})`.
 Since `(x : T | P)` uses `sig` directly,

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`::
 

doc/tools/docgram/fullGrammar

@@ -348,6 +348,7 @@ closed_binder: [
 | "`{" LIST1 typeclass_constraint SEP "," "}"
 | "`[" LIST1 typeclass_constraint SEP "," "]"
 | "'" pattern0
+| [ "of" | "&" ] term99
 ]
 
 one_open_binder: [

doc/tools/docgram/orderedGrammar

@@ -405,6 +405,7 @@ binder: [
 | generalizing_binder
 | "(" name ":" type "|" term ")"
 | "'" pattern0
+| [ "of" | "&" ] term99
 ]
 
 implicit_binders: [

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] }
+      | ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" ->
+        { [CLocalAssum ([CAst.make ~loc Anonymous], None, Default Explicit, c)] } ] ]
   ;
   one_open_binder:
     [ [ na = name -> { (pat_of_name na, Explicit) }

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   *)

test-suite/output/PrintKeywords.out

@@ -83,6 +83,7 @@ if
 in
 let
 match
+of
 return
 then
 using

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').

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 := {}.