[CS] support #[local] attribute

6 files changed, 43 insertions, 19 deletions

diff --git a/doc/changelog/07-commands-and-options/11162-local-cs.rst b/doc/changelog/07-commands-and-options/11162-local-cs.rst
new file mode 100644
index 0000000000..5a69a107cd
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11162-local-cs.rst
@@ -0,0 +1 @@
+- Handle the ``#[local]`` attribute in :g:`Canonical Structure` declarations (`#11162 <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi).
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index ae0afc7819..8caa289a47 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2003,10 +2003,11 @@ applied to an unknown structure instance (an implicit argument) and a
 value. The complete documentation of canonical structures can be found
 in :ref:`canonicalstructures`; here only a simple example is given.
 
-.. cmd:: Canonical {? Structure } @qualid
+.. cmd:: {? Local | #[local] } Canonical {? Structure } @qualid
 
    This command declares :token:`qualid` as a canonical instance of a
-   structure (a record).
+   structure (a record). When the :g:`#[local]` attribute is given the effect
+   stops at the end of the :g:`Section` containig it.
 
    Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
    structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
@@ -2069,7 +2070,7 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
       See :ref:`canonicalstructures` for a more realistic example.
 
-   .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term
+   .. cmdv:: {? Local | #[local] } Canonical {? Structure } @ident {? : @type } := @term
 
       This is equivalent to a regular definition of :token:`ident` followed by the
       declaration :n:`Canonical @ident`.
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index b8cae47196..e6d674c1e6 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -29,3 +29,25 @@ Canonical Structure bool_test := mk_test (fun x y => x || y).
 Definition b := bool.
 
 Check (fun x : b => x != x).
+
+Inductive four := x0 | x1 | x2 | x3.
+Structure local := MKL { l : four }.
+
+Section X.
+  Definition s0 := MKL x0.
+  #[local] Canonical Structure s0.
+  Check (refl_equal _ : l _ = x0).
+
+  #[local] Canonical Structure s1 := MKL x1.
+  Check (refl_equal _ : l _ = x1).
+
+  Local Canonical Structure s2 := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+
+End X.
+Fail Check (refl_equal _ : l _ = x0).
+Fail Check (refl_equal _ : l _ = x1).
+Fail Check (refl_equal _ : l _ = x2).
+Check s0.
+Check s1.
+Check s2.
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index e9454bab8a..141b02ef63 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -11,29 +11,30 @@ open Names
 open Libobject
 open Recordops
 
-let open_canonical_structure i (_, o) =
+let open_canonical_structure i (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
 
-let cache_canonical_structure (_, o) =
+let cache_canonical_structure (_, (o,_)) =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   register_canonical_structure ~warn:true env sigma o
 
-let discharge_canonical_structure (_,x) = Some x
+let discharge_canonical_structure (_,(x, local)) =
+  if local then None else Some (x, local)
 
-let inCanonStruc : Constant.t * inductive -> obj =
+let inCanonStruc : (Constant.t * inductive) * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
                   open_function = open_canonical_structure;
                   cache_function = cache_canonical_structure;
-                  subst_function = (fun (subst,c) -> subst_canonical_structure subst c);
+                  subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
                   classify_function = (fun x -> Substitute x);
                   discharge_function = discharge_canonical_structure }
 
 let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 
-let declare_canonical_structure ref =
+let declare_canonical_structure ?(local=false) ref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref)
+  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref, local)
diff --git a/vernac/canonical.mli b/vernac/canonical.mli
index a3bbaf6d18..e4161b4f97 100644
--- a/vernac/canonical.mli
+++ b/vernac/canonical.mli
@@ -9,4 +9,4 @@
 (************************************************************************)
 open Names
 
-val declare_canonical_structure : GlobRef.t -> unit
+val declare_canonical_structure : ?local:bool -> GlobRef.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f56cc00c3b..b53302e1d7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,11 +522,11 @@ 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 ~poly = let open Decls in function
+let vernac_definition_hook ~local ~poly = let open Decls in function
 | Coercion ->
   Some (Class.add_coercion_hook ~poly)
 | CanonicalStructure ->
-  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
+  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
   Some (Class.add_subclass_hook ~poly)
 | _ -> None
@@ -551,7 +551,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 ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~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 +560,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 ~poly:atts.polymorphic kind in
+  let hook = vernac_definition_hook ~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
@@ -1025,8 +1025,8 @@ let vernac_require from import qidl =
 
 (* Coercions and canonical structures *)
 
-let vernac_canonical r =
-  Canonical.declare_canonical_structure (smart_global r)
+let vernac_canonical ~local r =
+  Canonical.declare_canonical_structure ?local (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
@@ -2085,8 +2085,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         vernac_import export qidl)
   | VernacCanonical qid ->
     VtDefault(fun () ->
-        unsupported_attributes atts;
-        vernac_canonical qid)
+        vernac_canonical ~local:(only_locality atts) qid)
   | VernacCoercion (r,s,t) ->
     VtDefault(fun () -> vernac_coercion ~atts r s t)
   | VernacIdentityCoercion ({v=id},s,t) ->