aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-14 15:56:25 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-14 15:56:25 +0000
commit67f5c70a480c95cfb819fc68439781b5e5e95794 (patch)
tree67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /library/declaremods.mli
parentcc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff)
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r--library/declaremods.mli14
1 files changed, 7 insertions, 7 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli
index dedb9b67a..e52e2620a 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -64,14 +64,14 @@ val declare_module :
(env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
- identifier ->
- (identifier located list * ('modast annotated)) list ->
+ Id.t ->
+ (Id.t located list * ('modast annotated)) list ->
('modast annotated) module_signature ->
('modast annotated) list -> module_path
val start_module : (env -> 'modast -> module_struct_entry) ->
- bool option -> identifier ->
- (identifier located list * ('modast annotated)) list ->
+ bool option -> Id.t ->
+ (Id.t located list * ('modast annotated)) list ->
('modast annotated) module_signature -> module_path
val end_module : unit -> module_path
@@ -82,14 +82,14 @@ val end_module : unit -> module_path
val declare_modtype : (env -> 'modast -> module_struct_entry) ->
(env -> 'modast -> module_struct_entry * bool) ->
- identifier ->
- (identifier located list * ('modast annotated)) list ->
+ Id.t ->
+ (Id.t located list * ('modast annotated)) list ->
('modast annotated) list ->
('modast annotated) list ->
module_path
val start_modtype : (env -> 'modast -> module_struct_entry) ->
- identifier -> (identifier located list * ('modast annotated)) list ->
+ Id.t -> (Id.t located list * ('modast annotated)) list ->
('modast annotated) list -> module_path
val end_modtype : unit -> module_path