aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.mli
diff options
context:
space:
mode:
authorfilliatr1999-09-19 14:17:35 +0000
committerfilliatr1999-09-19 14:17:35 +0000
commit76e3b2928b766a76ee7e29dd3f6867cd48f95a52 (patch)
tree5a5a73ee8770cba524b8c24892f709a308e9ab3b /kernel/names.mli
parent5393ee683be9e19ab25888925f561ea4f4b1dddb (diff)
- un effort sur la doc (ocamlweb)
- module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.mli')
-rw-r--r--kernel/names.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index c022a84a3f..9a7822d117 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -24,6 +24,7 @@ val id_without_number : identifier -> bool
val first_char : identifier -> string
module Idset : Set.S with type elt = identifier
+module Idmap : Map.S with type key = identifier
val lift_ident : identifier -> identifier
val next_ident_away_from : identifier -> identifier list -> identifier