diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/attributes.ml | 4 | ||||
| -rw-r--r-- | vernac/attributes.mli | 3 | ||||
| -rw-r--r-- | vernac/canonical.ml | 8 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 19 |
7 files changed, 26 insertions, 18 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/himsg.ml b/vernac/himsg.ml index 085689be0a..ba7ae5069b 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -606,7 +606,7 @@ let rec explain_evar_kind env sigma evk ty = let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr env sigma evi.evar_concl with | Some _ -> - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in fnl () ++ str "Could not find an instance for " ++ pr_leconstr_env env sigma evi.evar_concl ++ pr_trailing_ne_context_of env sigma @@ -623,7 +623,7 @@ let explain_placeholder_kind env sigma c e = let explain_unsolvable_implicit env sigma evk explain = let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in let pe = pr_trailing_ne_context_of env sigma in strbrk "Cannot infer " ++ diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 8ced35c3be..b999ce9f3f 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -1003,9 +1003,7 @@ let print_canonical_projections env sigma grefs = | Const_cs y -> GlobRef.equal y gr | _ -> false end || - match gr with - | GlobRef.ConstRef con -> Names.Constant.equal c.o_ORIGIN con - | _ -> false + GlobRef.equal c.o_ORIGIN gr in let projs = List.filter (fun p -> List.for_all (match_proj_gref p) grefs) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 04f3e0d7b2..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)) @@ -474,7 +475,7 @@ let program_inference_hook env sigma ev = let tac = !Obligations.default_tactic in let evi = Evd.find sigma ev in let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env evi in + let env = Evd.evar_filtered_env env evi in try let concl = evi.Evd.evar_concl in if not (Evarutil.is_ground_env sigma env && @@ -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 |