diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 7 | ||||
| -rw-r--r-- | library/declare.mli | 5 |
2 files changed, 9 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index b53b19c353..307c838652 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -194,12 +194,15 @@ let declare_constant_common id discharged_hyps (cd,kind) = Dischargedhypsmap.set_discharged_hyps sp discharged_hyps; oname -let declare_constant id (cd,kind) = +let declare_constant_gen internal id (cd,kind) = let cd = hcons_constant_declaration cd in let oname = declare_constant_common id [] (ConstantEntry cd,kind) in - !xml_declare_constant oname; + !xml_declare_constant (internal,oname); oname +let declare_internal_constant = declare_constant_gen true +let declare_constant = declare_constant_gen false + (* when coming from discharge *) let redeclare_constant id discharged_hyps (cd,kind) = let _ = declare_constant_common id discharged_hyps (GlobalRecipe cd,kind) in diff --git a/library/declare.mli b/library/declare.mli index 77413640cb..9b268e7aea 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -54,6 +54,9 @@ type constant_declaration = constant_entry * global_kind the full path of the declaration *) val declare_constant : identifier -> constant_declaration -> object_name +val declare_internal_constant : + identifier -> constant_declaration -> object_name + val redeclare_constant : identifier -> Dischargedhypsmap.discharged_hyps -> Cooking.recipe * global_kind -> unit @@ -95,5 +98,5 @@ val strength_of_global : global_reference -> strength (* hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (object_name -> unit) -> unit +val set_xml_declare_constant : (bool * object_name -> unit) -> unit val set_xml_declare_inductive : (object_name -> unit) -> unit |