From 6aeea41c8a94233cb8b3ae15db1b20c75397610e Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 20 Sep 2001 16:31:09 +0000 Subject: Nettoyage des commentaires git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.mli | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index f525d49c7..0ae357c9c 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -79,14 +79,7 @@ val locate_section : qualid -> dir_path (* [exists sp] tells if [sp] is already bound to a cci term *) val exists_cci : section_path -> bool val exists_section : dir_path -> bool -(* -val open_module_contents : qualid -> unit -val rec_open_module_contents : qualid -> unit -(*s Entry points for sections *) -val open_section_contents : qualid -> unit -val push_section : section_path -> module_contents -> unit -*) (*s Roots of the space of absolute names *) (* This is the root of the standard library of Coq *) @@ -103,10 +96,6 @@ val push_library_root : module_ident -> unit references inside a block of mutual inductive *) val absolute_reference : section_path -> global_reference -(* -val is_absolute_dirpath : dir_path -> bool -*) - (* [locate_in_absolute_module dir id] finds [id] in module [dir] or in one of its section/subsection *) val locate_in_absolute_module : dir_path -> identifier -> global_reference -- cgit v1.2.3