diff options
| author | herbelin | 2003-06-10 21:05:01 +0000 |
|---|---|---|
| committer | herbelin | 2003-06-10 21:05:01 +0000 |
| commit | c76d3d5b03c45e0710f96089e0fb3abd7da67cd7 (patch) | |
| tree | 12581ab795ad429187c521eedba563bbb36df151 /library/libnames.mli | |
| parent | caebcb265c66bc69d5ce5d588cfdbe8bd27f31d4 (diff) | |
Passage des noms de tactiques à kernel_name pour compatibilité avec les foncteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libnames.mli')
| -rw-r--r-- | library/libnames.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/library/libnames.mli b/library/libnames.mli index e902cec9b4..95b47c52be 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -34,6 +34,9 @@ val reference_of_constr : constr -> global_reference module Refset : Set.S with type elt = global_reference module Refmap : Map.S with type key = global_reference +module Indmap : Map.S with type key = inductive +module Constrmap : Map.S with type key = constructor + (*s Dirpaths *) val pr_dirpath : dir_path -> Pp.std_ppcmds @@ -135,4 +138,3 @@ 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 - |