[Attributes] accept #[canonical] (Let|Definition)

7 files changed, 42 insertions, 9 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8caa289a47..05e4cf1346 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1994,6 +1994,8 @@ Deactivation of implicit arguments for parsing
    to be given as if no arguments were implicit. By symmetry, this also
    affects printing.
 
+.. _canonical-structure-declaration:
+
 Canonical structures
 ~~~~~~~~~~~~~~~~~~~~
 
@@ -2004,6 +2006,7 @@ value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
 .. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
+  :name: Canonical Structure
 
    This command declares :token:`qualid` as a canonical instance of a
    structure (a record). When the :g:`#[local]` attribute is given the effect
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 3cc101d06b..ac34fc707a 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1691,6 +1691,17 @@ variety of commands:
        :n:`@string__1` is the actual notation, :n:`@string__2` is the version number,
        :n:`@string__3` is the note.
 
+``canonical``
+    This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command.
+    It is equivalent to having a :cmd:`Canonical Structure` declaration just
+    after the command.
+
+    This attirbute can take the value ``false`` when decorating a record field
+    declaration with the effect of preventing the field from being involved in
+    the inference of canonical instances.
+
+    See also :ref:`canonical-structure-declaration`.
+
 .. example::
 
    .. coqtop:: all reset warn
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index bedb79d4d4..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -59,3 +59,14 @@ Section Y.
 End Y.
 Fail Check (refl_equal _ : l _ = x3).
 Fail Check s3.
+
+Section V.
+  #[canonical] Let s3 := MKL x3.
+  Check (refl_equal _ : l _ = x3).
+End V.
+
+Section W.
+  #[canonical, local] Definition s2' := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+End W.
+Fail Check (refl_equal _ : l _ = x2).
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index b7a3b002bd..68d2c3a00d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -234,5 +234,7 @@ let only_polymorphism atts = parse polymorphic atts
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
 let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
 
-let canonical =
+let canonical_field =
   enable_attribute ~key:"canonical" ~default:(fun () -> true)
+let canonical_instance =
+  enable_attribute ~key:"canonical" ~default:(fun () -> false)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 34ff15ca7d..0074db66d3 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -48,7 +48,8 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : Deprecation.t option attribute
-val canonical : bool attribute
+val canonical_field : bool attribute
+val canonical_instance : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 436648c163..975da64529 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -471,7 +471,7 @@ GRAMMAR EXTEND Gram
   [ [ attr = LIST0 quoted_attributes ;
       bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
       rf_notation = decl_notation -> {
-      let rf_canonical = attr |> List.flatten |> parse canonical in
+      let rf_canonical = attr |> List.flatten |> parse canonical_field in
       let rf_subclass, rf_decl = bd in
       rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 604d1b28ff..0acc2dd07c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -63,14 +63,15 @@ module DefAttributes = struct
     polymorphic : bool;
     program : bool;
     deprecated : Deprecation.t option;
+    canonical_instance : bool;
   }
 
   let parse f =
     let open Attributes in
-    let ((locality, deprecated), polymorphic), program =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+    let (((locality, deprecated), polymorphic), program), canonical_instance =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f
     in
-    { polymorphic; program; locality; deprecated }
+    { polymorphic; program; locality; deprecated; canonical_instance }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -522,13 +523,17 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   in
   start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
-let vernac_definition_hook ~local ~poly = let open Decls in function
+let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
   Some (ComCoercion.add_coercion_hook ~poly)
 | CanonicalStructure ->
   Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
   Some (ComCoercion.add_subclass_hook ~poly)
+| Definition when canonical_instance ->
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+| Let when canonical_instance ->
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
 | _ -> None
 
 let fresh_name_for_anonymous_theorem () =
@@ -551,7 +556,7 @@ let vernac_definition_name lid local =
 let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
@@ -560,7 +565,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let scope = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let name = vernac_definition_name lid scope in
   let red_option = match red_option with