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, 20 insertions, 1 deletions

diff --git a/library/libnames.mli b/library/libnames.mli
index 04e552f4d..e8dd2a5ff 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -10,7 +10,9 @@
 
 (*i*)
 open Pp
+open Util
 open Names
+open Term
 (*i*)
 
 (*s Global reference is a kernel side type for all references together *)
@@ -22,7 +24,14 @@ type global_reference =
 
 val subst_global : substitution -> global_reference -> global_reference
 
-(* dirpaths *)
+(* 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
+
+(*s Dirpaths *)
 val pr_dirpath : dir_path -> Pp.std_ppcmds
 
 val dirpath_of_string : string -> dir_path
@@ -111,3 +120,13 @@ type global_dir_reference =
   | DirModule of object_prefix
   | DirClosedSection of dir_path
       (* this won't last long I hope! *)
+
+type reference = 
+  | Qualid of qualid located
+  | Ident of identifier located
+
+val qualid_of_reference : reference -> qualid located
+val string_of_reference : reference -> string
+val pr_reference : reference -> std_ppcmds
+val loc_of_reference : reference -> loc
+