From 4425c8d353ffdcbed966c253f9624b550626ae0a Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 11 Mar 2013 20:14:31 +0000 Subject: Added a Local Definition vernacular command. This type of definition has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 1 + intf/decl_kinds.mli | 2 +- intf/vernacexpr.mli | 4 +- library/declare.ml | 67 ++++++++++------ library/declare.mli | 4 +- library/kindops.ml | 56 ++++++++++---- parsing/g_vernac.ml4 | 36 ++++----- plugins/funind/functional_principles_types.ml | 3 +- plugins/funind/indfun_common.ml | 19 +++-- pretyping/classops.ml | 95 ++++++++++++++--------- pretyping/classops.mli | 2 +- printing/ppvernac.ml | 18 +++-- tactics/leminv.ml | 20 +++-- tactics/tactics.ml | 17 ++-- toplevel/autoinstance.ml | 4 +- toplevel/class.ml | 70 ++++++++++------- toplevel/class.mli | 10 +-- toplevel/classes.ml | 39 +++++----- toplevel/command.ml | 107 ++++++++++++++------------ toplevel/ind_tables.ml | 22 +++--- toplevel/lemmas.ml | 67 +++++++++------- toplevel/obligations.ml | 6 +- toplevel/record.ml | 4 +- toplevel/vernacentries.ml | 10 ++- 24 files changed, 398 insertions(+), 285 deletions(-) diff --git a/CHANGES b/CHANGES index 065892e5a..6e4e9188b 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,7 @@ Vernacular commands A flag "Set/Unset Record Elimination Schemes" allows to change this. The tactic "induction" on a record is now actually doing "destruct". - The "Open Scope" command can now be given also a delimiter (e.g. Z). +- The "Definition" command now allows the "Local" modifier. Specification Language diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli index 91a03f675..7111fd055 100644 --- a/intf/decl_kinds.mli +++ b/intf/decl_kinds.mli @@ -8,7 +8,7 @@ (** Informal mathematical status of declarations *) -type locality = Local | Global +type locality = Discharge | Local | Global type binding_kind = Explicit | Implicit diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 4655e3588..a1eca85bc 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -252,9 +252,9 @@ type vernac_expr = export_flag option * lreference list | VernacImport of export_flag * lreference list | VernacCanonical of reference or_by_notation - | VernacCoercion of locality * reference or_by_notation * + | VernacCoercion of locality_flag * reference or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of locality * lident * + | VernacIdentityCoercion of locality_flag * lident * class_rawexpr * class_rawexpr (* Type classes *) diff --git a/library/declare.ml b/library/declare.ml index ee4656f75..ca18874d4 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -100,20 +100,30 @@ let declare_variable id obj = (** Declaration of constants and parameters *) +type constant_obj = { + cst_decl : global_declaration; + cst_hyps : Dischargedhypsmap.discharged_hyps; + cst_kind : logical_kind; + cst_locl : bool; +} + type constant_declaration = constant_entry * logical_kind (* At load-time, the segment starting from the module name to the discharge *) (* section (if Remark or Fact) is needed to access a construction *) -let load_constant i ((sp,kn),(_,_,kind)) = +let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then alreadydeclared (pr_id (basename sp) ++ str " already exists"); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (ConstRef con); - add_constant_kind con kind + add_constant_kind con obj.cst_kind (* Opening means making the name without its module qualification available *) -let open_constant i ((sp,kn),_) = - let con = Global.constant_of_delta_kn kn in +let open_constant i ((sp,kn), obj) = + (** Never open a local definition *) + if obj.cst_locl then () + else + let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = @@ -123,16 +133,16 @@ let check_exists sp = let id = basename sp in if exists_name id then alreadydeclared (pr_id id ++ str " already exists") -let cache_constant ((sp,kn),(cdt,dhyps,kind)) = +let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in - check_exists sp; - let kn' = Global.add_constant dir id cdt in + let () = check_exists sp in + let kn' = Global.add_constant dir id obj.cst_decl in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); add_section_constant kn' (Global.lookup_constant kn').const_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; - add_constant_kind (constant_of_kn kn) kind; + Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; + add_constant_kind (constant_of_kn kn) obj.cst_kind; !cache_hook sp let discharged_hyps kn sechyps = @@ -140,24 +150,28 @@ let discharged_hyps kn sechyps = let args = Array.to_list (instance_from_variable_context sechyps) in List.rev_map (Libnames.make_path dir) args -let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = +let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in let cb = Global.lookup_constant con in let repl = replacement_context () in let sechyps = section_segment_of_constant con in let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in - Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind) + let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in + let new_decl = GlobalRecipe recipe in + Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) -let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk +let dummy_constant cst = { + cst_decl = dummy_constant_entry; + cst_hyps = []; + cst_kind = cst.cst_kind; + cst_locl = cst.cst_locl; +} let classify_constant cst = Substitute (dummy_constant cst) -type constant_obj = - global_declaration * Dischargedhypsmap.discharged_hyps * logical_kind - let inConstant : constant_obj -> obj = declare_object { (default_object "CONSTANT") with cache_function = cache_constant; @@ -167,20 +181,27 @@ let inConstant : constant_obj -> obj = subst_function = ident_subst_function; discharge_function = discharge_constant } -let declare_constant_common id dhyps (cd,kind) = - let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in +let declare_constant_common id cst = + let (sp,kn) = add_leaf id (inConstant cst) in let c = Global.constant_of_delta_kn kn in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); c -let declare_constant ?(internal = UserVerbose) id (cd,kind) = - let kn = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant (internal,kn); +let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = + let cst = { + cst_decl = ConstantEntry cd; + cst_hyps = [] ; + cst_kind = kind; + cst_locl = local; + } in + let kn = declare_constant_common id cst in + let () = !xml_declare_constant (internal, kn) in kn -let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) +let declare_definition ?(internal=UserVerbose) + ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) id ?types body = let cb = { Entries.const_entry_body = body; @@ -189,8 +210,8 @@ let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds const_entry_inline_code = false; const_entry_secctx = None } in - declare_constant ~internal id - (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) + declare_constant ~internal ~local id + (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) diff --git a/library/declare.mli b/library/declare.mli index bcb72be58..fa9917a13 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -55,11 +55,11 @@ type internal_flag = | UserVerbose val declare_constant : - ?internal:internal_flag -> Id.t -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - Id.t -> ?types:constr -> constr -> constant + ?local:bool -> Id.t -> ?types:constr -> constr -> constant (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of diff --git a/library/kindops.ml b/library/kindops.ml index 35aebc531..6e6c7527b 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,18 +24,44 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - match def with - | Local, Coercion -> "Coercion Local" - | Global, Coercion -> "Coercion" - | Local, Definition -> "Let" - | Global, Definition -> "Definition" - | Local, SubClass -> "Local SubClass" - | Global, SubClass -> "SubClass" - | Global, CanonicalStructure -> "Canonical Structure" - | Global, Example -> "Example" - | Local, (CanonicalStructure|Example) -> - Errors.anomaly (Pp.str "Unsupported local definition kind") - | Local, Instance -> "Instance" - | Global, Instance -> "Global Instance" - | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) - -> Errors.anomaly (Pp.str "Internal definition kind") + let (locality, kind) = def in + let error () = Errors.anomaly (Pp.str "Internal definition kind") in + match kind with + | Definition -> + begin match locality with + | Discharge -> "Let" + | Local -> "Local Definition" + | Global -> "Definition" + end + | Example -> + begin match locality with + | Discharge -> error () + | Local -> "Local Example" + | Global -> "Example" + end + | Coercion -> + begin match locality with + | Discharge -> error () + | Local -> "Local Coercion" + | Global -> "Coercion" + end + | SubClass -> + begin match locality with + | Discharge -> error () + | Local -> "Local SubClass" + | Global -> "SubClass" + end + | CanonicalStructure -> + begin match locality with + | Discharge -> error () + | Local -> error () + | Global -> "Canonical Structure" + end + | Instance -> + begin match locality with + | Discharge -> error () + | Local -> "Instance" + | Global -> "Global Instance" + end + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + Errors.anomaly (Pp.str "Internal definition kind") diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 47d1796ce..e6f7480b6 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -196,26 +196,26 @@ GEXTEND Gram ; def_token: [ [ "Definition" -> - (Global, Definition) + (use_locality_exp (), Definition) | IDENT "Let" -> - (Local, Definition) + (Discharge, Definition) | IDENT "Example" -> - (Global, Example) + (use_locality_exp (), Example) | IDENT "SubClass" -> (use_locality_exp (), SubClass) ] ] ; assumption_token: - [ [ "Hypothesis" -> (Local, Logical) - | "Variable" -> (Local, Definitional) - | "Axiom" -> (Global, Logical) - | "Parameter" -> (Global, Definitional) - | IDENT "Conjecture" -> (Global, Conjectural) ] ] + [ [ "Hypothesis" -> (Discharge, Logical) + | "Variable" -> (Discharge, Definitional) + | "Axiom" -> (use_locality_exp (), Logical) + | "Parameter" -> (use_locality_exp (), Definitional) + | IDENT "Conjecture" -> (use_locality_exp (), Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Local, Logical) - | IDENT "Variables" -> (Local, Definitional) - | IDENT "Axioms" -> (Global, Logical) - | IDENT "Parameters" -> (Global, Definitional) ] ] + [ [ IDENT "Hypotheses" -> (Discharge, Logical) + | IDENT "Variables" -> (Discharge, Definitional) + | IDENT "Axioms" -> (use_locality_exp (), Logical) + | IDENT "Parameters" -> (use_locality_exp (), Definitional) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> Some (int_of_string i) @@ -544,22 +544,22 @@ GEXTEND Gram VernacDefinition ((enforce_locality_exp true,Coercion),(Loc.ghost,s),d) | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (enforce_locality_exp true, f, s, t) + VernacIdentityCoercion (enforce_locality true, f, s, t) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (use_locality_exp (), f, s, t) + VernacIdentityCoercion (use_locality (), f, s, t) | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality_exp true, AN qid, s, t) + VernacCoercion (enforce_locality true, AN qid, s, t) | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (enforce_locality_exp true, ByNotation ntn, s, t) + VernacCoercion (enforce_locality true, ByNotation ntn, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality_exp (), AN qid, s, t) + VernacCoercion (use_locality (), AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (use_locality_exp (), ByNotation ntn, s, t) + VernacCoercion (use_locality (), ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index debf96345..7f05c3b0e 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -348,8 +348,7 @@ let generate_functional_principle Declare.declare_constant name (Entries.DefinitionEntry ce, - Decl_kinds.IsDefinition (Decl_kinds.Scheme) - ) + Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; names := name :: !names diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 9879f08a0..8305c4735 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -148,25 +148,28 @@ open Declare let definition_message = Declare.definition_message +let get_locality = function +| Discharge -> true +| Local -> true +| Global -> false + let save with_clean id const (locality,kind) hook = let {const_entry_body = pft; const_entry_secctx = _; const_entry_type = tpo; const_entry_opaque = opacity } = const in let l,r = match locality with - | Local when Lib.sections_are_opened () -> + | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in let c = SectionLocalDef (pft, tpo, opacity) in let _ = declare_variable id (Lib.cwd(), c, k) in (Local, VarRef id) - | Local -> - let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) - | Global -> + | Discharge | Local | Global -> + let local = get_locality locality in let k = Kindops.logical_kind_of_goal_kind kind in - let kn = declare_constant id (DefinitionEntry const, k) in - (Global, ConstRef kn) in + let kn = declare_constant id ~local (DefinitionEntry const, k) in + (locality, ConstRef kn) + in if with_clean then Pfedit.delete_current_proof (); hook l r; definition_message id diff --git a/pretyping/classops.ml b/pretyping/classops.ml index d2334583a..907034d47 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -44,14 +44,14 @@ module CoeTypMap = Refmap_env type coe_info_typ = { coe_value : constr; coe_type : types; - coe_strength : locality; + coe_local : bool; coe_is_identity : bool; coe_param : int } let coe_info_typ_equal c1 c2 = eq_constr c1.coe_value c2.coe_value && eq_constr c1.coe_type c2.coe_type && - c1.coe_strength == c2.coe_strength && + c1.coe_local == c2.coe_local && c1.coe_is_identity == c2.coe_is_identity && Int.equal c1.coe_param c2.coe_param @@ -342,7 +342,14 @@ let add_coercion_in_graph (ic,source,target) = if is_ambig && is_verbose () then msg_warning (message_ambig !ambig_paths) -type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int +type coercion = { + coercion_type : coe_typ; + coercion_local : bool; + coercion_is_id : bool; + coercion_source : cl_typ; + coercion_target : cl_typ; + coercion_params : int; +} (* Calcul de l'arit้ d'une classe *) @@ -373,18 +380,18 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) = - add_class cls; - add_class clt; - let is,_ = class_info cls in - let it,_ = class_info clt in +let cache_coercion (_, c) = + let () = add_class c.coercion_source in + let () = add_class c.coercion_target in + let is, _ = class_info c.coercion_source in + let it, _ = class_info c.coercion_target in let xf = - { coe_value = constr_of_global coe; - coe_type = Global.type_of_global coe; - coe_strength = stre; - coe_is_identity = isid; - coe_param = ps } in - add_new_coercion coe xf; + { coe_value = constr_of_global c.coercion_type; + coe_type = Global.type_of_global c.coercion_type; + coe_local = c.coercion_local; + coe_is_identity = c.coercion_is_id; + coe_param = c.coercion_params } in + let () = add_new_coercion c.coercion_type xf in add_coercion_in_graph (xf,is,it) let load_coercion _ o = @@ -399,34 +406,38 @@ let open_coercion i o = then cache_coercion o -let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) = - let coe' = subst_coe_typ subst coe in - let cls' = subst_cl_typ subst cls in - let clt' = subst_cl_typ subst clt in - if coe' == coe && cls' == cls & clt' == clt then obj else - (coe',stre,isid,cls',clt',ps) +let subst_coercion (subst, c) = + let coe = subst_coe_typ subst c.coercion_type in + let cls = subst_cl_typ subst c.coercion_source in + let clt = subst_cl_typ subst c.coercion_target in + if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt then c + else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt } + let discharge_cl = function | CL_CONST kn -> CL_CONST (Lib.discharge_con kn) | CL_IND ind -> CL_IND (Lib.discharge_inductive ind) | cl -> cl -let discharge_coercion (_,(coe,stre,isid,cls,clt,ps)) = - match stre with - | Local -> None - | Global -> - let n = try Array.length (Lib.section_instance coe) with Not_found -> 0 in - Some (Lib.discharge_global coe, - stre, - isid, - discharge_cl cls, - discharge_cl clt, - n + ps) - -let classify_coercion (coe,stre,isid,cls,clt,ps as obj) = - match stre with - | Local -> Dispose - | Global -> Substitute obj +let discharge_coercion (_, c) = + if c.coercion_local then None + else + let n = + try + let ins = Lib.section_instance c.coercion_type in + Array.length ins + with Not_found -> 0 + in + let nc = { c with + coercion_type = Lib.discharge_global c.coercion_type; + coercion_source = discharge_cl c.coercion_source; + coercion_target = discharge_cl c.coercion_target; + coercion_params = n + c.coercion_params; + } in + Some nc + +let classify_coercion obj = + if obj.coercion_local then Dispose else Substitute obj let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with @@ -437,8 +448,16 @@ let inCoercion : coercion -> obj = classify_function = classify_coercion; discharge_function = discharge_coercion } -let declare_coercion coef stre ~isid ~src:cls ~target:clt ~params:ps = - Lib.add_anonymous_leaf (inCoercion (coef,stre,isid,cls,clt,ps)) +let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps = + let c = { + coercion_type = coef; + coercion_local = local; + coercion_is_id = isid; + coercion_source = cls; + coercion_target = clt; + coercion_params = ps; + } in + Lib.add_anonymous_leaf (inCoercion c) (* For printing purpose *) let get_coercion_value v = v.coe_value diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 82af9d418..8f36e95e6 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -65,7 +65,7 @@ val class_args_of : env -> evar_map -> types -> constr list (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *) val declare_coercion : - coe_typ -> locality -> isid:bool -> + coe_typ -> ?local:bool -> isid:bool -> src:cl_typ -> target:cl_typ -> params:int -> unit (** {6 Access to coercions infos } *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 4a91e1284..850ad2b75 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -327,16 +327,20 @@ let pr_class_rawexpr = function | RefClass qid -> pr_smart_global qid let pr_assumption_token many = function - | (Local,Logical) -> + | (Discharge,Logical) -> str (if many then "Hypotheses" else "Hypothesis") - | (Local,Definitional) -> + | (Discharge,Definitional) -> str (if many then "Variables" else "Variable") | (Global,Logical) -> str (if many then "Axioms" else "Axiom") | (Global,Definitional) -> str (if many then "Parameters" else "Parameter") + | (Local, Logical) -> + str (if many then "Local Axioms" else "Local Axiom") + | (Local,Definitional) -> + str (if many then "Local Parameters" else "Local Parameter") | (Global,Conjectural) -> str"Conjecture" - | (Local,Conjectural) -> + | ((Discharge | Local),Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture") let pr_params pr_c (xl,(c,t)) = @@ -706,14 +710,14 @@ let rec pr_vernac = function | VernacCanonical q -> str"Canonical Structure" ++ spc() ++ pr_smart_global q | VernacCoercion (s,id,c1,c2) -> hov 1 ( - str"Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ + str"Coercion" ++ (if s then spc() ++ + str"Local" ++ spc() else spc()) ++ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) | VernacIdentityCoercion (s,id,c1,c2) -> hov 1 ( - str"Identity Coercion" ++ (match s with | Local -> spc() ++ - str"Local" ++ spc() | Global -> spc()) ++ pr_lident id ++ + str"Identity Coercion" ++ (if s then spc() ++ + str"Local" ++ spc() else spc()) ++ pr_lident id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 942cdc77e..c8a3ffd55 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -225,17 +225,15 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in - let _ = - declare_constant name - (DefinitionEntry - { const_entry_body = invProof; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false; - const_entry_inline_code = false - }, - IsProof Lemma) - in () + let entry = { + const_entry_body = invProof; + const_entry_secctx = None; + const_entry_type = None; + const_entry_opaque = false; + const_entry_inline_code = false; + } in + let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in + () (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ba5e0e04..a3733b3e7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3528,7 +3528,10 @@ let abstract_subproof id tac gl = let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in - let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in + let decl = (cd, IsProof Lemma) in + (** ppedrot: seems legit to have abstracted subproofs as local*) + let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in + let lem = mkConst cst in exact_no_check (applist (lem,List.rev (Array.to_list (instance_from_named_context sign)))) gl @@ -3556,12 +3559,12 @@ let admit_as_an_axiom gl = let na = next_global_ident_away name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; - let axiom = - let cd = - Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in - let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in - constr_of_global (ConstRef con) - in + let entry = (Pfedit.get_used_variables (), concl, None) in + let cd = Entries.ParameterEntry entry in + let decl = (cd, IsAssumption Logical) in + (** ppedrot: seems legit to have admitted subproofs as local*) + let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in + let axiom = constr_of_global (ConstRef con) in exact_no_check (applist (axiom, List.rev (Array.to_list (instance_from_named_context sign)))) 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 *) -- cgit v1.2.3