diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/autoinstance.ml | 4 | ||||
-rw-r--r-- | toplevel/class.ml | 70 | ||||
-rw-r--r-- | toplevel/class.mli | 10 | ||||
-rw-r--r-- | toplevel/classes.ml | 39 | ||||
-rw-r--r-- | toplevel/command.ml | 107 | ||||
-rw-r--r-- | toplevel/ind_tables.ml | 22 | ||||
-rw-r--r-- | toplevel/lemmas.ml | 67 | ||||
-rw-r--r-- | toplevel/obligations.ml | 6 | ||||
-rw-r--r-- | toplevel/record.ml | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 10 |
10 files changed, 189 insertions, 150 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 3eb77bc06..97d655da5 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -184,8 +184,8 @@ let declare_record_instance gr ctx params = const_entry_type=None; const_entry_opaque=false; const_entry_inline_code = false } in - let cst = Declare.declare_constant ident - (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in + let decl = (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in + let cst = Declare.declare_constant ident decl in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def let declare_class_instance gr ctx params = diff --git a/toplevel/class.ml b/toplevel/class.ml index 9d93d39f6..8f8f70816 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -20,7 +20,9 @@ open Globnames open Nametab open Decl_kinds -let strength_min l = if List.mem Local l then Local else Global +let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL + +let loc_of_bool b = if b then `LOCAL else `GLOBAL (* Errors *) @@ -147,13 +149,13 @@ let prods_of t = aux [] t let strength_of_cl = function - | CL_CONST kn -> Global - | CL_SECVAR id -> Local - | _ -> Global + | CL_CONST kn -> `GLOBAL + | CL_SECVAR id -> `LOCAL + | _ -> `GLOBAL let strength_of_global = function - | VarRef _ -> Local - | _ -> Global + | VarRef _ -> `LOCAL + | _ -> `GLOBAL let get_strength stre ref cls clt = let stres = strength_of_cl cls in @@ -220,7 +222,8 @@ let build_id_coercion idf_opt source = const_entry_opaque = false; const_entry_inline_code = true } in - let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in + let decl = (constr_entry, IsDefinition IdentityCoercion) in + let kn = declare_constant idf decl in ConstRef kn let check_source = function @@ -263,37 +266,50 @@ let add_new_coercion_core coef stre source target isid = check_target clt target; check_arity cls; check_arity clt; - let stre' = get_strength stre coef cls clt in - declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs) + let local = match get_strength stre coef cls clt with + | `LOCAL -> true + | `GLOBAL -> false + in + declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs) -let try_add_new_coercion_core ref b c d e = - try add_new_coercion_core ref b c d e +let try_add_new_coercion_core ref ~local c d e = + try add_new_coercion_core ref (loc_of_bool local) c d e with CoercionError e -> errorlabstrm "try_add_new_coercion_core" (explain_coercion_error ref e ++ str ".") -let try_add_new_coercion ref stre = - try_add_new_coercion_core ref stre None None false +let try_add_new_coercion ref ~local = + try_add_new_coercion_core ref ~local None None false -let try_add_new_coercion_subclass cl stre = +let try_add_new_coercion_subclass cl ~local = let coe_ref = build_id_coercion None cl in - try_add_new_coercion_core coe_ref stre (Some cl) None true + try_add_new_coercion_core coe_ref ~local (Some cl) None true -let try_add_new_coercion_with_target ref stre ~source ~target = - try_add_new_coercion_core ref stre (Some source) (Some target) false +let try_add_new_coercion_with_target ref ~local ~source ~target = + try_add_new_coercion_core ref ~local (Some source) (Some target) false -let try_add_new_identity_coercion id stre ~source ~target = +let try_add_new_identity_coercion id ~local ~source ~target = let ref = build_id_coercion (Some id) source in - try_add_new_coercion_core ref stre (Some source) (Some target) true - -let try_add_new_coercion_with_source ref stre ~source = - try_add_new_coercion_core ref stre (Some source) None false + try_add_new_coercion_core ref ~local (Some source) (Some target) true -let add_coercion_hook stre ref = - try_add_new_coercion ref stre; - Flags.if_verbose msg_info - (pr_global_env Id.Set.empty ref ++ str " is now a coercion") +let try_add_new_coercion_with_source ref ~local ~source = + try_add_new_coercion_core ref ~local (Some source) None false -let add_subclass_hook stre ref = +let add_coercion_hook local ref = + let stre = match local with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let () = try_add_new_coercion ref stre in + let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + Flags.if_verbose msg_info msg + +let add_subclass_hook local ref = + let stre = match local with + | Local -> true + | Global -> false + | Discharge -> assert false + in let cl = class_of_global ref in try_add_new_coercion_subclass cl stre diff --git a/toplevel/class.mli b/toplevel/class.mli index a72ec1a81..0d39ee170 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -18,28 +18,28 @@ open Nametab (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion from [src] to [tg] *) -val try_add_new_coercion_with_target : global_reference -> locality -> +val try_add_new_coercion_with_target : global_reference -> local:bool -> source:cl_typ -> target:cl_typ -> unit (** [try_add_new_coercion ref s] declares [ref], assumed to be of type [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *) -val try_add_new_coercion : global_reference -> locality -> unit +val try_add_new_coercion : global_reference -> local:bool -> unit (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a transparent constant which unfolds to some class [tg]; it declares an identity coercion from [cst] to [tg], named something like ["Id_cst_tg"] *) -val try_add_new_coercion_subclass : cl_typ -> locality -> unit +val try_add_new_coercion_subclass : cl_typ -> local:bool -> unit (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion from [src] to [tg] where the target is inferred from the type of [ref] *) -val try_add_new_coercion_with_source : global_reference -> locality -> +val try_add_new_coercion_with_source : global_reference -> local:bool -> source:cl_typ -> unit (** [try_add_new_identity_coercion id s src tg] enriches the environment with a new definition of name [id] declared as an identity coercion from [src] to [tg] *) -val try_add_new_identity_coercion : Id.t -> locality -> +val try_add_new_identity_coercion : Id.t -> local:bool -> source:cl_typ -> target:cl_typ -> unit val add_coercion_hook : unit Tacexpr.declaration_hook diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 03fc6bd1f..570e66deb 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -99,16 +99,15 @@ let instance_hook k pri global imps ?hook cst = (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k pri global imps ?hook id term termtype = - let cdecl = - let kind = IsDefinition Instance in - let entry = - { const_entry_body = term; - const_entry_secctx = None; - const_entry_type = Some termtype; - const_entry_opaque = false; - const_entry_inline_code = false } - in DefinitionEntry entry, kind + let kind = IsDefinition Instance in + let entry = { + const_entry_body = term; + const_entry_secctx = None; + const_entry_type = Some termtype; + const_entry_opaque = false; + const_entry_inline_code = false } in + let cdecl = (DefinitionEntry entry, kind) in let kn = Declare.declare_constant id cdecl in Declare.definition_message id; instance_hook k pri global imps ?hook (ConstRef kn); @@ -321,27 +320,27 @@ let context l = let _, ((env', fullctx), impls) = interp_context_evars evars env l in let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in let ce t = Evarutil.check_evars env Evd.empty !evars t in - List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx; + let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in let ctx = try named_of_rel_context fullctx with _ -> error "Anonymous variables not allowed in contexts." in let fn status (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let cst = Declare.declare_constant ~internal:Declare.KernelSilent id - (ParameterEntry (None,t,None), IsAssumption Logical) - in + let decl = (ParameterEntry (None,t,None), IsAssumption Logical) in + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id decl in match class_of_constr t with | Some (rels, (tc, args) as _cl) -> add_instance (Typeclasses.new_instance tc None false (ConstRef cst)); status (* declare_subclasses (ConstRef cst) cl *) | None -> status - else ( - let impl = List.exists - (fun (x,_) -> - match x with ExplByPos (_, Some id') -> Id.equal id id' | _ -> false) impls + else + let test (x, _) = match x with + | ExplByPos (_, Some id') -> Id.equal id id' + | _ -> false in - Command.declare_assumption false (Local (* global *), Definitional) t - [] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status) + let impl = List.exists test impls in + let decl = (Discharge, Definitional) in + let nstatus = Command.declare_assumption false decl t [] impl None (Loc.ghost, id) in + status && nstatus in List.fold_left fn true (List.rev ctx) - diff --git a/toplevel/command.ml b/toplevel/command.ml index d5a1da6d0..21bb963db 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -112,35 +112,43 @@ let check_definition (ce, evd, imps) = Option.iter (check_evars env Evd.empty evd) ce.const_entry_type; ce +let get_locality id = function +| Discharge -> + (** If a Let is defined outside a section, then we consider it as a local definition *) + let msg = pr_id id ++ strbrk " is declared as a local definition" in + let () = if Flags.is_verbose () then msg_warning msg in + true +| Local -> true +| Global -> false + let declare_global_definition ident ce local k imps = - let kn = declare_constant ident (DefinitionEntry ce,IsDefinition k) in + let local = get_locality ident local in + let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr imps; - if local == Local && Flags.is_verbose() then - msg_warning (pr_id ident ++ strbrk " is declared as a global definition"); - definition_message ident; - Autoinstance.search_declaration (ConstRef kn); - gr + let () = maybe_declare_manual_implicits false gr imps in + let () = definition_message ident in + let () = Autoinstance.search_declaration (ConstRef kn) in + gr let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ident (local,k) ce imps hook = - !declare_definition_hook ce; +let declare_definition ident (local, k) ce imps hook = + let () = !declare_definition_hook ce in let r = match local with - | Local when Lib.sections_are_opened () -> - let c = - SectionLocalDef(ce.const_entry_body ,ce.const_entry_type,false) in - let _ = declare_variable ident (Lib.cwd(),c,IsDefinition k) in - definition_message ident; - if Pfedit.refining () then - Flags.if_warn msg_warning - (strbrk "Local definition " ++ pr_id ident ++ - strbrk " is not visible from current goals"); - VarRef ident - | (Global|Local) -> - declare_global_definition ident ce local k imps in + | Discharge when Lib.sections_are_opened () -> + let c = SectionLocalDef(ce.const_entry_body, ce.const_entry_type, false) in + let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in + let () = definition_message ident in + let () = if Pfedit.refining () then + let msg = strbrk "Section definition " ++ + pr_id ident ++ strbrk " is not visible from current goals" in + Flags.if_warn msg_warning msg + in + VarRef ident + | Discharge | Local | Global -> + declare_global_definition ident ce local k imps in hook local r let _ = Obligations.declare_definition_ref := declare_definition @@ -158,40 +166,37 @@ let do_definition ident k bl red_option c ctypopt hook = let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in - ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls) + ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in declare_definition ident k ce imps hook (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) -let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = - let r,status = match local with - | Local when Lib.sections_are_opened () -> - let _ = - declare_variable ident - (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in - assumption_message ident; - if is_verbose () && Pfedit.refining () then - msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ - strbrk " is not visible from current goals"); - let r = VarRef ident in - Typeclasses.declare_instance None true r; r,true - | (Global|Local) -> - let kn = - declare_constant ident - (ParameterEntry (None,c,nl), IsAssumption kind) in - let gr = ConstRef kn in - maybe_declare_manual_implicits false gr imps; - assumption_message ident; - if local == Local && Flags.is_verbose () then - msg_warning (pr_id ident ++ strbrk " is declared as a parameter" ++ - strbrk " because it is at a global level"); - Autoinstance.search_declaration (ConstRef kn); - Typeclasses.declare_instance None false gr; - gr , (Lib.is_modtype_strict ()) +let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match local with +| Discharge when Lib.sections_are_opened () -> + let decl = (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in + let _ = declare_variable ident decl in + let () = assumption_message ident in + let () = + if is_verbose () && Pfedit.refining () then + msg_warning (str"Variable" ++ spc () ++ pr_id ident ++ + strbrk " is not visible from current goals") in - if is_coe then Class.try_add_new_coercion r local; - status + let r = VarRef ident in + let () = Typeclasses.declare_instance None true r in + let () = if is_coe then Class.try_add_new_coercion r ~local:true in + true +| Global | Local | Discharge -> + let local = get_locality ident local in + let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in + let kn = declare_constant ident ~local decl in + let gr = ConstRef kn in + let () = maybe_declare_manual_implicits false gr imps in + let () = assumption_message ident in + let () = Autoinstance.search_declaration (ConstRef kn) in + let () = Typeclasses.declare_instance None false gr in + let () = if is_coe then Class.try_add_new_coercion gr local in + Lib.is_modtype_strict () let declare_assumptions_hook = ref ignore let set_declare_assumptions_hook = (:=) declare_assumptions_hook @@ -399,7 +404,7 @@ let do_mutual_inductive indl finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false) coes (* 3c| Fixpoints and co-fixpoints *) @@ -510,6 +515,7 @@ let declare_fix kind f def t imps = const_entry_opaque = false; const_entry_inline_code = false } in + (** FIXME: include locality *) let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in Autoinstance.search_declaration (ConstRef kn); @@ -704,6 +710,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = const_entry_opaque = false; const_entry_inline_code = false} in + (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in if Impargs.is_implicit_args () || not (List.is_empty impls) then diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index e03c3e9b5..7cf60b7ff 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -123,18 +123,18 @@ let compute_name internal id = let define internal id c = let fd = declare_constant ~internal in let id = compute_name internal id in - let kn = fd id - (DefinitionEntry - { const_entry_body = c; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false; - const_entry_inline_code = false - }, - Decl_kinds.IsDefinition Scheme) in - (match internal with + let entry = { + const_entry_body = c; + const_entry_secctx = None; + const_entry_type = None; + const_entry_opaque = false; + const_entry_inline_code = false + } in + let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in + let () = match internal with | KernelSilent -> () - | _-> definition_message id); + | _-> definition_message id + in kn let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) = diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index bf8cbcc25..e1f17b571 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -166,14 +166,18 @@ let save id const do_guard (locality,kind) hook = const_entry_opaque = opacity } = const in let k = Kindops.logical_kind_of_goal_kind kind in let l,r = match locality with - | Local when Lib.sections_are_opened () -> + | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef (pft, tpo, opacity) in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) - | Local | Global -> - let kn = declare_constant id (DefinitionEntry const, k) in + | Local | Global | Discharge -> + let local = match locality with + | Local | Discharge -> true + | Global -> false + in + let kn = declare_constant id ~local (DefinitionEntry const, k) in Autoinstance.search_declaration (ConstRef kn); - (Global, ConstRef kn) in + (locality, ConstRef kn) in Pfedit.delete_current_proof (); definition_message id; hook l r @@ -191,41 +195,51 @@ let compute_proof_name locality = function | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) -let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) = +let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = match body with | None -> - (match local with - | Local -> - let impl=false in (* copy values from Vernacentries *) + (match locality with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) let k = IsAssumption Conjectural in let c = SectionLocalAssum (t_i,impl) in let _ = declare_variable id (Lib.cwd(),c,k) in - (Local,VarRef id,imps) - | Global -> + (Discharge, VarRef id,imps) + | Local | Global -> let k = IsAssumption Conjectural in - let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in - (Global,ConstRef kn,imps)) + let local = match locality with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let decl = (ParameterEntry (None,t_i,None), k) in + let kn = declare_constant id ~local decl in + (locality,ConstRef kn,imps)) | Some body -> let k = Kindops.logical_kind_of_goal_kind kind in let body_i = match kind_of_term body with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) | _ -> anomaly (Pp.str "Not a proof by induction") in - match local with - | Local -> + match locality with + | Discharge -> let c = SectionLocalDef (body_i, Some t_i, opaq) in let _ = declare_variable id (Lib.cwd(), c, k) in - (Local,VarRef id,imps) - | Global -> - let const = - { const_entry_body = body_i; - const_entry_secctx = None; - const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_inline_code = false - } in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global,ConstRef kn,imps) + (Discharge,VarRef id,imps) + | Local | Global -> + let local = match locality with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let const = { const_entry_body = body_i; + const_entry_secctx = None; + const_entry_type = Some t_i; + const_entry_opaque = opaq; + const_entry_inline_code = false + } in + let kn = declare_constant id ~local (DefinitionEntry const, k) in + (locality,ConstRef kn,imps) let save_hook = ref ignore let set_save_hook f = save_hook := f @@ -345,8 +359,7 @@ let start_proof_com kind thms hook = let admit () = let (id,k,typ,hook) = Pfedit.current_proof_statement () in let e = Pfedit.get_used_variables(), typ, None in - let kn = - declare_constant id (ParameterEntry e,IsAssumption Conjectural) in + let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in Pfedit.delete_current_proof (); assumption_message id; hook Global (ConstRef kn) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index b4384e77b..74b387dfe 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -590,7 +590,8 @@ let declare_obligation prg obl body = const_entry_opaque = opaque; const_entry_inline_code = false} in - let constant = Declare.declare_constant obl.obl_name + (** ppedrot: seems legit to have obligations as local *) + let constant = Declare.declare_constant obl.obl_name ~local:true (DefinitionEntry ce,IsProof Property) in if not opaque then @@ -945,7 +946,8 @@ let admit_prog prg = match x.obl_body with | None -> let x = subst_deps_obl obls x in - let kn = Declare.declare_constant x.obl_name + (** ppedrot: seems legit to have admitted obligations as local *) + let kn = Declare.declare_constant x.obl_name ~local:true (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural) in assumption_message x.obl_name; diff --git a/toplevel/record.ml b/toplevel/record.ml index 93868dbe3..b6181590e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -214,7 +214,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls Impargs.maybe_declare_manual_implicits false refi impls; if coe then begin let cl = Class.class_of_global (IndRef indsp) in - Class.try_add_new_coercion_with_source refi Global ~source:cl + Class.try_add_new_coercion_with_source refi ~local:false ~source:cl end; let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in let constr_fip = applist (constr_fi,proj_args) in @@ -273,7 +273,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls let cstr = (rsp,1) in let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in let build = ConstructRef cstr in - if is_coe then Class.try_add_new_coercion build Global; + let () = if is_coe then Class.try_add_new_coercion build ~local:false in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); if infer then Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign (); diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index e735dde0d..4c5e07a54 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -459,8 +459,10 @@ let vernac_definition_hook = function let vernac_definition (local,k) (loc,id as lid) def = let hook = vernac_definition_hook k in - if local == Local then Dumpglob.dump_definition lid true "var" - else Dumpglob.dump_definition lid false "def"; + let () = match local with + | Discharge -> Dumpglob.dump_definition lid true "var" + | Local | Global -> Dumpglob.dump_definition lid false "def" + in (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local,DefinitionBody Definition) @@ -768,13 +770,13 @@ let vernac_coercion stre ref qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in - Class.try_add_new_coercion_with_target ref' stre ~source ~target; + Class.try_add_new_coercion_with_target ref' ~local:stre ~source ~target; if_verbose msg_info (pr_global ref' ++ str " is now a coercion") let vernac_identity_coercion stre id qids qidt = let target = cl_of_qualid qidt in let source = cl_of_qualid qids in - Class.try_add_new_identity_coercion id stre ~source ~target + Class.try_add_new_identity_coercion id ~local:stre ~source ~target (* Type classes *) |