[CS] support #[local] attribute

3 files changed, 16 insertions, 16 deletions

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