diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
| commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
| tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /library/libnames.mli | |
| parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) | |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index b93ee87ee..43ca252c1 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -47,7 +47,7 @@ val global_of_constr : constr -> global_reference val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference -module Refset : Set.S with type elt = global_reference +module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference (*s Extended global references *) @@ -65,7 +65,7 @@ val dirpath_of_string : string -> dir_path val string_of_dirpath : dir_path -> string (* Pop the suffix of a [dir_path] *) -val pop_dirpath : dir_path -> dir_path +val pop_dirpath : dir_path -> dir_path (* Pop the suffix n times *) val pop_dirpath_n : int -> dir_path -> dir_path @@ -146,7 +146,7 @@ type object_prefix = dir_path * (module_path * dir_path) val make_oname : object_prefix -> identifier -> object_name (* to this type are mapped [dir_path]'s in the nametab *) -type global_dir_reference = +type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix @@ -158,7 +158,7 @@ type global_dir_reference = global name (referred either by a qualified name or by a single name) or a variable *) -type reference = +type reference = | Qualid of qualid located | Ident of identifier located |