diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-30 11:00:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-30 11:00:04 +0000 |
| commit | f5e8da3bbf50e7a826398a05ba7c5cfafe667a6e (patch) | |
| tree | c9b90cac2d4155763e413a518f729032f1c60f71 /library | |
| parent | d7a64f8b6efd748625c8eb9aa2aef08ca618e5c6 (diff) | |
Distinction entre declarations internes (p.ex. _subproof) et declarations utilisateurs pour export xml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
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 b53b19c35..307c83865 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 77413640c..9b268e7ae 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 |