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

7 files changed, 19 insertions, 13 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index b120a95bc8..6ac022c2d3 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -488,7 +488,7 @@ let print_object_kind uri (xmltag,variation) =
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-let print glob_ref xml_library_root =
+let print internal glob_ref xml_library_root =
  let module D = Declarations in
  let module De = Declare in
  let module G = Global in
@@ -526,7 +526,7 @@ let print glob_ref xml_library_root =
   in
   let fn = filename_of_path ~keep_sections xml_library_root kn tag in
   let uri = Cic2acic.uri_of_kernel_name ~keep_sections kn tag in
-   print_object_kind uri (kind_of_object glob_ref);
+   if not internal then print_object_kind uri (kind_of_object glob_ref);
    print_object uri obj Evd.empty None fn
 ;;
 
@@ -847,15 +847,15 @@ let _ =
 let _ =
   Declare.set_xml_declare_variable
    (function (sp,kn) ->
-      print (Libnames.VarRef (Libnames.basename sp)) xml_library_root)
+      print false (Libnames.VarRef (Libnames.basename sp)) xml_library_root)
 ;;
 
 let _ =
   Declare.set_xml_declare_constant
-   (function (sp,kn) ->
+   (function (internal,(sp,kn)) ->
      match !proof_to_export with
         None ->
-          print (Libnames.ConstRef kn) xml_library_root
+          print internal (Libnames.ConstRef kn) xml_library_root
       | Some pftreestate ->
          (* It is a proof. Let's export it starting from the proof-tree *)
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
@@ -868,7 +868,7 @@ let _ =
 let _ =
   Declare.set_xml_declare_inductive
    (function (sp,kn) ->
-      print (Libnames.IndRef (kn,0)) xml_library_root)
+      print false (Libnames.IndRef (kn,0)) xml_library_root)
 ;;
 
 let _ =
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index ed3713ff75..535bb915a2 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -28,7 +28,7 @@
 (* Note: it is printed only (and directly) the most discharged available  *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-val print : Libnames.global_reference -> string option -> unit
+val print : bool -> Libnames.global_reference -> string option -> unit
 
 (* show dest                                                  *)
 (*  where dest is either None (for stdout) or (Some filename) *)
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index 267e45a837..27ae9fc376 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -39,7 +39,7 @@ END
 
 (* Print XML and Show XML *)
 
-let print_global r fn = Xmlcommand.print (Nametab.global r) fn
+let print_global r fn = Xmlcommand.print false (Nametab.global r) fn
 
 VERNAC COMMAND EXTEND Xml
 | [ "Print" "XML" filename(fn) global(qid) ] -> [ print_global qid fn ]
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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 695bb3bc7a..989944ae99 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1904,7 +1904,7 @@ let abstract_subproof name tac gls =
 	(delete_current_proof(); raise e)
     in   (* Faudrait un peu fonctionnaliser cela *)
     let cd = Entries.DefinitionEntry const in
-    let sp = Declare.declare_constant na (cd,IsProof Lemma) in
+    let sp = Declare.declare_internal_constant na (cd,IsProof Lemma) in
     let newenv = Global.env() in
     constr_of_reference (ConstRef (snd sp))
   in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4ecca992dc..9d4e9d68d4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -185,7 +185,7 @@ let declare_one_elimination ind =
   let mindstr = string_of_id mip.mind_typename in
   let declare s c t =
     let id = id_of_string s in
-    let kn = Declare.declare_constant id
+    let kn = Declare.declare_internal_constant id
       (DefinitionEntry
         { const_entry_body = c;
           const_entry_type = t;