aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES1
-rw-r--r--intf/decl_kinds.mli2
-rw-r--r--intf/vernacexpr.mli4
-rw-r--r--library/declare.ml67
-rw-r--r--library/declare.mli4
-rw-r--r--library/kindops.ml56
-rw-r--r--parsing/g_vernac.ml436
-rw-r--r--plugins/funind/functional_principles_types.ml3
-rw-r--r--plugins/funind/indfun_common.ml19
-rw-r--r--pretyping/classops.ml95
-rw-r--r--pretyping/classops.mli2
-rw-r--r--printing/ppvernac.ml18
-rw-r--r--tactics/leminv.ml20
-rw-r--r--tactics/tactics.ml17
-rw-r--r--toplevel/autoinstance.ml4
-rw-r--r--toplevel/class.ml70
-rw-r--r--toplevel/class.mli10
-rw-r--r--toplevel/classes.ml39
-rw-r--r--toplevel/command.ml107
-rw-r--r--toplevel/ind_tables.ml22
-rw-r--r--toplevel/lemmas.ml67
-rw-r--r--toplevel/obligations.ml6
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/vernacentries.ml10
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:04:04 +0000