Merge PR #11164: [CS] allow Let variable to be canonical

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: ppedrot

5 files changed, 22 insertions, 12 deletions

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/canonical.ml b/vernac/canonical.ml
index 141b02ef63..e41610b532 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -21,10 +21,12 @@ let cache_canonical_structure (_, (o,_)) =
   let sigma = Evd.from_env env in
   register_canonical_structure ~warn:true env sigma o
 
-let discharge_canonical_structure (_,(x, local)) =
-  if local then None else Some (x, local)
+let discharge_canonical_structure (_,((gref, _ as x), local)) =
+  if local || (Globnames.isVarRef gref && Lib.is_in_section gref) then None
+  else Some (x, local)
 
-let inCanonStruc : (Constant.t * inductive) * bool -> obj =
+
+let inCanonStruc : (GlobRef.t * inductive) * bool -> obj =
   declare_object {(default_object "CANONICAL-STRUCTURE") with
                   open_function = open_canonical_structure;
                   cache_function = cache_canonical_structure;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 69ab0fafe9..3302231fd1 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 99d74f16cc..e98820bc98 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