diff options
| -rw-r--r-- | library/declare.ml | 7 | ||||
| -rw-r--r-- | library/declare.mli | 12 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | toplevel/classes.ml | 4 | ||||
| -rw-r--r-- | toplevel/ind_tables.ml | 6 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 9 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
8 files changed, 18 insertions, 28 deletions
diff --git a/library/declare.ml b/library/declare.ml index b0af8d518..0764af4b0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -172,17 +172,12 @@ let declare_constant_common id dhyps (cd,kind) = Notation.declare_ref_arguments_scope (ConstRef c); c -let declare_constant_gen internal id (cd,kind) = +let declare_constant ?(internal = UserVerbose) id (cd,kind) = let cd = hcons_constant_declaration cd in let kn = declare_constant_common id [] (ConstantEntry cd,kind) in !xml_declare_constant (internal,kn); kn -(* TODO: add a third function to distinguish between KernelVerbose - * and user Verbose *) -let declare_internal_constant = declare_constant_gen KernelSilent -let declare_constant = declare_constant_gen UserVerbose - (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = diff --git a/library/declare.mli b/library/declare.mli index b6ed0a815..1ad733816 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -43,17 +43,19 @@ 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 - the full path of the declaration *) + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent + + *) type internal_flag = | KernelVerbose | KernelSilent | UserVerbose val declare_constant : - identifier -> constant_declaration -> constant - -val declare_internal_constant : - identifier -> constant_declaration -> constant + ?internal:internal_flag -> identifier -> constant_declaration -> 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/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index c792367c3..0e9281a21 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1464,7 +1464,7 @@ let add_morphism_infer glob m n = let instance_id = add_suffix n "_Proper" in let instance = build_morphism_signature m in if Lib.is_modtype () then - let cst = Declare.declare_internal_constant instance_id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2069cc23f..b253b2375 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3473,7 +3473,7 @@ let abstract_subproof id tac gl = let const = Pfedit.build_constant_by_tactic secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in - let lem = mkConst (Declare.declare_internal_constant id (cd,IsProof Lemma)) in + let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in exact_no_check (applist (lem,List.rev (Array.to_list (instance_from_named_context sign)))) gl @@ -3503,7 +3503,7 @@ let admit_as_an_axiom gl = if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = let cd = Entries.ParameterEntry (concl,false) in - let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in constr_of_global (ConstRef con) in exact_no_check diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ea3a888ec..c06fbfc68 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props Evarutil.nf_evar !evars t in Evarutil.check_evars env Evd.empty !evars termtype; - let cst = Declare.declare_internal_constant id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None false imps ?hook (ConstRef cst); id end @@ -301,7 +301,7 @@ let context ?(hook=fun _ -> ()) l = in let fn (id, _, t) = if Lib.is_modtype () && not (Lib.sections_are_opened ()) then - let cst = Declare.declare_internal_constant id + let cst = Declare.declare_constant ~internal:Declare.KernelSilent id (ParameterEntry (t,false), IsAssumption Logical) in match class_of_constr t with diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 974b74a6d..3440f9fe8 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -110,11 +110,7 @@ let declare_scheme kind indcl = Lib.add_anonymous_leaf (inScheme (kind,indcl)) let define internal id c = - (* TODO: specify even more by distinguish between KernelVerbose and - * UserVerbose *) - let fd = match internal with - | KernelSilent -> declare_internal_constant - | _ -> declare_constant in + let fd = declare_constant ~internal in let kn = fd id (DefinitionEntry { const_entry_body = c; diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 3b090e79e..8d8997a2b 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -79,7 +79,7 @@ let _ = (* compatibility *) let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 -let eq_dec_flag = ref false +let eq_dec_flag = ref false let _ = declare_bool_option { optsync = true; @@ -100,10 +100,7 @@ let _ = (* Util *) let define id internal c t = - (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) - let f = match internal with - | KernelSilent -> declare_internal_constant - | _ -> declare_constant in + let f = declare_constant ~internal in let kn = f id (DefinitionEntry { const_entry_body = c; @@ -121,8 +118,8 @@ let declare_beq_scheme_gen internal names kn = let alarm what internal msg = let debug = false in - (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *) match internal with + | KernelVerbose | KernelSilent -> (if debug then Flags.if_verbose Pp.msg_warning diff --git a/toplevel/record.ml b/toplevel/record.ml index 0b338fdd8..0dd18f064 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -193,7 +193,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls const_entry_opaque = false; const_entry_boxed = Flags.boxed_definitions() } in let k = (DefinitionEntry cie,IsDefinition kind) in - let kn = declare_internal_constant fid k in + let kn = declare_constant ~internal:KernelSilent fid k in Flags.if_verbose message (string_of_id fid ^" is defined"); kn with Type_errors.TypeError (ctx,te) -> |