Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 10 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 3c04ddf57..3a7849232 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -92,13 +92,6 @@ val clear_proofs : named_context -> named_context
 
 val context_of_global_reference : global_reference -> section_context
 
-(* Turn a global reference into a construction *)
-val constr_of_reference : global_reference -> constr
-
-(* Turn a construction denoting a global into a reference;
-   raise [Not_found] if not a global *)
-val reference_of_constr : constr -> global_reference
-
 val global_qualified_reference : qualid -> constr
 val global_absolute_reference : section_path -> constr
 val global_reference_in_absolute_module : dir_path -> identifier -> constr
@@ -120,6 +113,6 @@ val strength_of_global : global_reference -> strength
 val library_part : global_reference -> dir_path
 
 (* hooks for XML output *)
-val set_xml_declare_variable : (kernel_name -> unit) -> unit
-val set_xml_declare_constant : (kernel_name -> unit) -> unit
-val set_xml_declare_inductive : (kernel_name -> unit) -> unit
+val set_xml_declare_variable : (object_name -> unit) -> unit
+val set_xml_declare_constant : (object_name -> unit) -> unit
+val set_xml_declare_inductive : (object_name -> unit) -> unit