From b91f60aab99980b604dc379b4ca62f152315c841 Mon Sep 17 00:00:00 2001 From: barras Date: Mon, 5 Nov 2001 16:48:30 +0000 Subject: GROS COMMIT: - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.mli | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 5fb7eb237..6cf3f8673 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -17,6 +17,16 @@ open Names (*s This module contains the table for globalization, which associates global names (section paths) to qualified names. *) +type global_reference = + | VarRef of variable + | ConstRef of constant + | IndRef of inductive + | ConstructRef of constructor + +(* Finds the real name of a global (e.g. fetch the constructor names + from the inductive name and constructor number) *) +val sp_of_global : Environ.env -> global_reference -> section_path + type extended_global_reference = | TrueGlobal of global_reference | SyntacticDef of section_path @@ -33,9 +43,11 @@ val make_short_qualid : identifier -> qualid val string_of_qualid : qualid -> string val pr_qualid : qualid -> std_ppcmds -(* Turns an absolute name into a qualified name denoting the same name *) val qualid_of_sp : section_path -> qualid +(* Turns an absolute name into a qualified name denoting the same name *) +val qualid_of_global : Environ.env -> global_reference -> qualid + exception GlobalizationError of qualid exception GlobalizationConstantError of qualid @@ -56,7 +68,7 @@ val push_short_name_object : section_path -> unit val push_section : dir_path -> unit (* This should eventually disappear *) -val sp_of_id : path_kind -> identifier -> global_reference +val sp_of_id : identifier -> global_reference (*s The following functions perform globalization of qualified names *) @@ -83,15 +95,6 @@ val exists_section : dir_path -> bool (*s Roots of the space of absolute names *) -(* This is the root of the standard library of Coq *) -val coq_root : module_ident - -(* This is the default root prefix for developments which doesn't mention a root *) -val default_root_prefix : dir_path - -(* This is to declare a new root *) -val push_library_root : dir_path -> unit - (* This turns a "user" absolute name into a global reference; especially, constructor/inductive names are turned into internal references inside a block of mutual inductive *) -- cgit v1.2.3