From e88e0b2140bdd2d194a52bc09f8338b5667d0f92 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 14 Nov 2002 18:37:54 +0000 Subject: 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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.mli | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'library/libnames.mli') 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 + -- cgit v1.2.3