aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/tacinv.ml42
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/interface/xlate.ml21
-rw-r--r--contrib/recdef/recdef.ml410
-rw-r--r--contrib/subtac/rewrite.ml4
-rw-r--r--contrib/xml/xmlcommand.ml29
-rw-r--r--library/declare.ml8
-rw-r--r--library/declare.mli8
-rw-r--r--parsing/ppvernac.ml19
-rw-r--r--tactics/setoid_replace.ml10
-rw-r--r--tactics/tacinterp.ml5
-rw-r--r--tactics/tactics.ml2
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/command.ml50
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml9
16 files changed, 74 insertions, 109 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index bf918ba56..c2410d55c 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -842,7 +842,7 @@ let declareFunScheme f fname mutflist =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = true } in
- let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition)) in
+ let _= ignore (declare_constant fname (DefinitionEntry ce,IsDefinition Scheme)) in
()
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 50c8a0fa1..b06ba1992 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -140,7 +140,7 @@ let make_variable_ast name typ implicits =
let make_definition_ast name c typ implicits =
- VernacDefinition ((Global,Definition false), (dummy_loc,name), DefineBody ([], None,
+ VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
(constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
(fun _ _ -> ()))
::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ea7b52162..f17cb67b4 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1361,24 +1361,9 @@ let coerce_genarg_to_VARG x =
| ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
-let xlate_thm x = CT_thm (match x with
- | Theorem -> "Theorem"
- | Remark -> "Remark"
- | Lemma -> "Lemma"
- | Fact -> "Fact")
-
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition _) -> "Local"
- | (Global, Definition true) -> "Boxed Definition"
- | (Global, Definition false) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) ->
- xlate_error "Local CanonicalStructure not parsed")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
+
+let xlate_defn k = CT_defn (string_of_definition_kind k)
let xlate_var x = CT_var (match x with
| (Global,Definitional) -> "Parameter"
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 2e62aa407..32febb6fa 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -694,7 +694,7 @@ let new_com_terminate fonctional_ref input_type relation_ast rec_arg_num
let (evmap, env) = Command.get_current_context() in
let (relation:constr)= interp_constr evmap env relation_ast in
(start_proof thm_name
- (IsGlobal (Proof Lemma)) (Environ.named_context_val env)
+ (Global, Proof Lemma) (Environ.named_context_val env)
(new_hyp_terminates fonctional_ref) hook;
by (new_whole_start fonctional_ref
input_type relation rec_arg_num ));;
@@ -762,7 +762,7 @@ let (value_f:constr list -> global_reference -> constr) =
in
understand Evd.empty (Global.env()) value;;
-let (declare_fun : identifier -> global_kind -> constr -> global_reference) =
+let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
fun f_id kind value ->
let ce = {const_entry_body = value;
const_entry_type = None;
@@ -770,7 +770,7 @@ let (declare_fun : identifier -> global_kind -> constr -> global_reference) =
const_entry_boxed = true} in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let (declare_f : identifier -> global_kind -> constr list -> global_reference -> global_reference) =
+let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -943,7 +943,7 @@ let (com_eqn : identifier ->
let (evmap, env) = Command.get_current_context() in
let eq_constr = interp_constr evmap env eq in
let f_constr = (constr_of_reference f_ref) in
- (start_proof eq_name (IsGlobal (Proof Lemma))
+ (start_proof eq_name (Global, Proof Lemma)
(Environ.named_context_val env) eq_constr (fun _ _ -> ());
by
(start_equation f_ref terminate_ref
@@ -978,7 +978,7 @@ let recursive_definition f type_of_f r rec_arg_num eq =
let equation_id = add_suffix f "_equation" in
let functional_id = add_suffix f "_F" in
let term_id = add_suffix f "_terminate" in
- let functional_ref = declare_fun functional_id IsDefinition res in
+ let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
let hook _ _ =
let term_ref = Nametab.locate (make_short_qualid term_id) in
let f_ref = declare_f f (IsProof Lemma) arg_types term_ref in
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index 201f2d48b..afbbd18af 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -539,8 +539,8 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
in aux ctx t
-let global_kind : Decl_kinds.global_kind = Decl_kinds.IsDefinition
-let goal_kind = Decl_kinds.IsGlobal Decl_kinds.DefinitionBody
+let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
let make_fixpoint t id term =
let term' = mkLambda (Name id, t.f_fulltype, term) in
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 96f73abe0..39a12a7ea 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -434,16 +434,10 @@ let theory_output_string ?(do_not_quote = false) s =
Buffer.add_string theory_buffer s
;;
-let kind_of_theorem = function
- | Decl_kinds.Theorem -> "Theorem"
- | Decl_kinds.Lemma -> "Lemma"
- | Decl_kinds.Fact -> "Fact"
- | Decl_kinds.Remark -> "Remark"
-
let kind_of_global_goal = function
- | Decl_kinds.IsGlobal Decl_kinds.DefinitionBody -> "DEFINITION","InteractiveDefinition"
- | Decl_kinds.IsGlobal (Decl_kinds.Proof k) -> "THEOREM",kind_of_theorem k
- | Decl_kinds.IsLocal -> assert false
+ | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
+ | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
+ | Decl_kinds.Local, _ -> assert false
let kind_of_inductive isrecord kn =
"DEFINITION",
@@ -458,8 +452,9 @@ let kind_of_variable id =
| DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
| DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
| DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
- | DK.IsDefinition -> "VARIABLE","LocalDefinition"
- | DK.IsProof DK.LocalStatement -> "VARIABLE","LocalFact"
+ | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
+ | DK.IsProof _ -> "VARIABLE","LocalFact"
+ | _ -> Util.anomaly "Unsupported variable kind"
;;
let kind_of_constant kn =
@@ -468,8 +463,10 @@ let kind_of_constant kn =
| DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
| DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
| DK.IsAssumption DK.Conjectural -> "AXIOM","Conjecture"
- | DK.IsDefinition -> "DEFINITION","Definition"
- | DK.IsProof thm -> "THEOREM",kind_of_theorem thm
+ | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
+ | DK.IsDefinition DK.Example -> "DEFINITION","Example"
+ | DK.IsDefinition _ -> Util.anomaly "Unsupported constant kind"
+ | DK.IsProof thm -> "THEOREM",DK.string_of_theorem_kind thm
;;
let kind_of_global r =
@@ -560,10 +557,10 @@ let show_pftreestate internal fn (kind,pftst) id =
let kn = Lib.make_kn id in
let env = Global.env () in
let obj =
- mk_current_proof_obj (kind = Decl_kinds.IsLocal) id val0 typ evar_map env in
+ mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in
let uri =
match kind with
- Decl_kinds.IsLocal ->
+ Decl_kinds.Local, _ ->
let uri =
"cic:/" ^ String.concat "/"
(Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable)
@@ -571,7 +568,7 @@ let show_pftreestate internal fn (kind,pftst) id =
let kind_of_var = "VARIABLE","LocalFact" in
if not internal then print_object_kind uri kind_of_var;
uri
- | Decl_kinds.IsGlobal _ ->
+ | Decl_kinds.Global, _ ->
let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in
if not internal then print_object_kind uri (kind_of_global_goal kind);
uri
diff --git a/library/declare.ml b/library/declare.ml
index 5359290be..3835180b1 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -59,14 +59,14 @@ type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
| SectionLocalAssum of types
-type variable_declaration = dir_path * section_variable_entry * local_kind
+type variable_declaration = dir_path * section_variable_entry * logical_kind
type checked_section_variable =
| CheckedSectionLocalDef of constr * types * Univ.constraints * bool
| CheckedSectionLocalAssum of types * Univ.constraints
type checked_variable_declaration =
- dir_path * checked_section_variable * local_kind
+ dir_path * checked_section_variable * logical_kind
let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
@@ -123,9 +123,9 @@ let declare_variable id obj =
(* Globals: constants and parameters *)
-type constant_declaration = constant_entry * global_kind
+type constant_declaration = constant_entry * logical_kind
-let csttab = ref (Spmap.empty : global_kind Spmap.t)
+let csttab = ref (Spmap.empty : logical_kind Spmap.t)
let _ = Summary.declare_summary "CONSTANT"
{ Summary.freeze_function = (fun () -> !csttab);
diff --git a/library/declare.mli b/library/declare.mli
index 317c27281..f04170b34 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -36,14 +36,14 @@ type section_variable_entry =
| SectionLocalDef of constr * types option * bool (* opacity *)
| SectionLocalAssum of types
-type variable_declaration = dir_path * section_variable_entry * local_kind
+type variable_declaration = dir_path * section_variable_entry * logical_kind
val declare_variable : variable -> variable_declaration -> object_name
(* Declaration of global constructions *)
(* i.e. Definition/Theorem/Axiom/Parameter/... *)
-type constant_declaration = constant_entry * global_kind
+type constant_declaration = constant_entry * logical_kind
(* [declare_constant id cd] declares a global declaration
(constant/parameter) with name [id] in the current section; it returns
@@ -66,11 +66,11 @@ val string_of_strength : strength -> string
val is_constant : section_path -> bool
val constant_strength : section_path -> strength
-val constant_kind : section_path -> global_kind
+val constant_kind : section_path -> logical_kind
val get_variable : variable -> named_declaration
val variable_strength : variable -> strength
-val variable_kind : variable -> local_kind
+val variable_kind : variable -> logical_kind
val find_section_variable : variable -> section_path
val last_section_hyps : dir_path -> identifier list
val clear_proofs : named_context -> Environ.named_context_val
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 378417a12..e7fc0e01f 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -323,11 +323,7 @@ let pr_ne_params_list pr_c l =
prlist_with_sep pr_semicolon (pr_params pr_c)
*)
-let pr_thm_token = function
- | Theorem -> str"Theorem"
- | Lemma -> str"Lemma"
- | Fact -> str"Fact"
- | Remark -> str"Remark"
+let pr_thm_token k = str (string_of_theorem_kind k)
let pr_syntax_modifier = function
| SetItemLevel (l,NextLevel) ->
@@ -481,18 +477,7 @@ let rec pr_vernac = function
(* Gallina *)
| VernacDefinition (d,id,b,f) -> (* A verifier... *)
- let pr_def_token = function
- | Local, Coercion -> str"Coercion Local"
- | Global, Coercion -> str"Coercion"
- | Local, Definition _ -> str"Let"
- | Global, Definition b ->
- if b then str"Boxed Definition"
- else str"Definition"
- | Local, SubClass -> str"Local SubClass"
- | Global, SubClass -> str"SubClass"
- | Global, CanonicalStructure -> str"Canonical Structure"
- | Local, CanonicalStructure ->
- anomaly "Don't know how to translate a local canonical structure" in
+ let pr_def_token dk = str (string_of_definition_kind dk) in
let pr_reduce = function
| None -> mt()
| Some r ->
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index cc58983bd..50261ed97 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -688,7 +688,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
- IsDefinition)) ;
+ IsDefinition Definition)) ;
mext
in
let mmor = current_constant mor_name in
@@ -926,7 +926,7 @@ let new_morphism m signature id hook =
begin
new_edited id
(m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
- Pfedit.start_proof id (IsGlobal (Proof Lemma))
+ Pfedit.start_proof id (Global, Proof Lemma)
(Declare.clear_proofs (Global.named_context ()))
lem hook;
Options.if_verbose msg (Printer.pr_open_subgoals ());
@@ -1047,7 +1047,7 @@ let int_add_relation id a aeq refl sym trans =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
- IsDefinition) in
+ IsDefinition Definition) in
let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
let xreflexive_relation_class =
let subst =
@@ -1064,7 +1064,7 @@ let int_add_relation id a aeq refl sym trans =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() },
- IsDefinition) in
+ IsDefinition Definition) in
let aeq_rel =
{ aeq_rel with
rel_X_relation_class = current_constant id;
@@ -1124,7 +1124,7 @@ let int_add_relation id a aeq refl sym trans =
const_entry_type = None;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()},
- IsDefinition)
+ IsDefinition Definition)
in
let a_quantifiers_rev =
List.map (fun (n,b,t) -> assert (b = None); n,t) a_quantifiers_rev in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7eff2b69f..aa36074d2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1175,7 +1175,8 @@ let solvable_by_tactic env evi (ev,args) src =
Environ.named_context_of_val evi.evar_hyps =
Environ.named_context env ->
let id = id_of_string "H" in
- start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ());
+ start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl
+ (fun _ _ -> ());
begin
try
by (tclCOMPLETE tac);
@@ -1520,7 +1521,7 @@ and interp_letin ist gl = function
try
let t = tactic_of_value v in
let ndc = Environ.named_context_val env in
- start_proof id IsLocal ndc typ (fun _ _ -> ());
+ start_proof id (Local,Proof Lemma) ndc typ (fun _ _ -> ());
by t;
let (_,({const_entry_body = pft},_,_)) = cook_proof () in
delete_proof (dummy_loc,id);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f57b490fc..bbc359ef0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1816,7 +1816,7 @@ let abstract_subproof name tac gls =
if occur_existential concl then
error "\"abstract\" cannot handle existentials";
let lemme =
- start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ());
+ start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ());
let _,(const,kind,_) =
try
by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac));
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 8512e00c5..436aa8409 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -248,7 +248,7 @@ let build_id_coercion idf_opt source =
const_entry_type = Some typ_f;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions()} in
- let kn = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+ let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
ConstRef kn
let check_source = function
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 74494429c..811989600 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -129,26 +129,20 @@ let red_constant_entry bl ce = function
body }
let declare_global_definition ident ce local =
- let kn = declare_constant ident (DefinitionEntry ce,IsDefinition) in
+ let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
if local = Local then
msg_warning (pr_id ident ++ str" is declared as a global definition");
definition_message ident;
ConstRef kn
-let is_boxed_def dok =
- match dok with
- | Definition b -> b
- | _ -> false
-
-let declare_definition ident (local,dok) bl red_option c typopt hook =
- let boxed = is_boxed_def dok in
+let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
let ce' = red_constant_entry bl ce red_option 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) in
+ let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
definition_message ident;
if Pfedit.refining () then
msgerrnl (str"Warning: Local definition " ++ pr_id ident ++
@@ -212,7 +206,7 @@ let declare_one_elimination ind =
const_entry_type = t;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() },
- Decl_kinds.IsDefinition) in
+ Decl_kinds.IsDefinition Definition) in
definition_message id;
kn
in
@@ -507,8 +501,8 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
- let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
- (ConstRef kn)
+ let kn = declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+ in (ConstRef kn)
in
(* declare the recursive definitions *)
let lrefrec = Array.mapi declare namerec in
@@ -522,7 +516,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
const_entry_type = Some t;
const_entry_opaque = false;
const_entry_boxed = boxed } in
- let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in
+ let _ =
+ declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+ in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -573,8 +569,8 @@ let build_corecursive lnameardef boxed =
const_entry_opaque = false;
const_entry_boxed = boxed }
in
- let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
- (ConstRef kn)
+ let kn = declare_constant fi (DefinitionEntry ce,IsDefinition CoFixpoint)
+ in (ConstRef kn)
in
let lrefrec = Array.mapi declare namerec in
if_verbose ppnl (corecursive_message lrefrec);
@@ -586,7 +582,8 @@ let build_corecursive lnameardef boxed =
const_entry_type = Some t;
const_entry_opaque = false;
const_entry_boxed = boxed } in
- let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in
+ let _ =
+ declare_constant f (DefinitionEntry ce,IsDefinition Definition) in
warning ((string_of_id f)^" is non-recursively defined");
(var_subst f) :: subst)
(List.map var_subst (Array.to_list namerec))
@@ -613,7 +610,7 @@ let build_scheme lnamedepindsort =
const_entry_type = Some decltype;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() } in
- let kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+ let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in
ConstRef kn :: lrecref
in
let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -640,21 +637,22 @@ let start_proof_com sopt kind (bl,t) hook =
let _ = Typeops.infer_type env c in
start_proof id kind c hook
-let save id const kind hook =
+let save id const (locality,kind) hook =
let {const_entry_body = pft;
const_entry_type = tpo;
const_entry_opaque = opacity } = const in
- let l,r = match kind with
- | IsLocal when Lib.sections_are_opened () ->
+ let l,r = match locality with
+ | Local when Lib.sections_are_opened () ->
+ let k = logical_kind_of_goal_kind kind in
let c = SectionLocalDef (pft, tpo, opacity) in
- let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in
+ let _ = declare_variable id (Lib.cwd(), c, k) in
(Local, VarRef id)
- | IsLocal ->
- let k = IsDefinition in
+ | Local ->
+ let k = logical_kind_of_goal_kind kind in
let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn)
- | IsGlobal k ->
- let k = theorem_kind_of_goal_kind k in
+ | Global ->
+ let k = logical_kind_of_goal_kind kind in
let kn = declare_constant id (DefinitionEntry const, k) in
(Global, ConstRef kn) in
hook l r;
@@ -684,7 +682,7 @@ let save_anonymous_with_strength kind opacity save_ident =
let const = { const with const_entry_opaque = opacity } in
check_anonymity id save_ident;
(* we consider that non opaque behaves as local for discharge *)
- save save_ident const (IsGlobal (Proof kind)) hook
+ save save_ident const (Global, Proof kind) hook
let admit () =
let (id,k,typ,hook) = Pfedit.current_proof_statement () in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 2378edf6d..f4f0c9150 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -166,7 +166,7 @@ let declare_projections indsp coers fields =
const_entry_type = Some projtyp;
const_entry_opaque = false;
const_entry_boxed = Options.boxed_definitions() } in
- let k = (DefinitionEntry cie,IsDefinition) in
+ let k = (DefinitionEntry cie,IsDefinition StructureComponent) in
let kn = declare_internal_constant fid k in
Options.if_verbose message (string_of_id fid ^" is defined");
kn
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c08b52727..77075e2fa 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -304,7 +304,7 @@ let start_proof_and_print idopt k t hook =
print_subgoals ();
if !pcoq <> None then (out_some !pcoq).start_proof ()
-let vernac_definition (local,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) id def hook =
match def with
| ProveBody (bl,t) -> (* local binders, typ *)
if Lib.is_modtype () then
@@ -312,8 +312,7 @@ let vernac_definition (local,_ as k) id def hook =
(str "Proof editing mode not supported in module types")
else
let hook _ _ = () in
- let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in
- start_proof_and_print (Some id) kind (bl,t) hook
+ start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
| DefineBody (bl,red_option,c,typ_opt) ->
let red_option = match red_option with
| None -> None
@@ -330,7 +329,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
if Lib.is_modtype () then
errorlabstrm "Vernacentries.StartProof"
(str "Proof editing mode not supported in module types");
- start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
+ start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
let vernac_end_proof = function
| Admitted -> admit ()
@@ -939,7 +938,7 @@ let vernac_goal = function
| Some c ->
if not (refining()) then begin
let unnamed_kind = Lemma (* Arbitrary *) in
- start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->());
+ start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
print_subgoals ()
end else
error "repeated Goal not permitted in refining mode"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 19:44:00 +0000