diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/library/global.mli b/library/global.mli index 82b7cc8eb..fdada3f87 100644 --- a/library/global.mli +++ b/library/global.mli @@ -35,22 +35,22 @@ val named_context : unit -> Sign.named_context val env_is_empty : unit -> bool (** {6 Extending env with variables and local definitions } *) -val push_named_assum : (identifier * types) -> Univ.constraints -val push_named_def : (identifier * constr * types option) -> Univ.constraints +val push_named_assum : (Id.t * types) -> Univ.constraints +val push_named_def : (Id.t * constr * types option) -> Univ.constraints (** {6 ... } *) (** Adding constants, inductives, modules and module types. All these functions verify that given names match those generated by kernel *) val add_constant : - dir_path -> identifier -> global_declaration -> constant + dir_path -> Id.t -> global_declaration -> constant val add_mind : - dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive + dir_path -> Id.t -> mutual_inductive_entry -> mutual_inductive val add_module : - identifier -> module_entry -> inline -> module_path * delta_resolver + Id.t -> module_entry -> inline -> module_path * delta_resolver val add_modtype : - identifier -> module_struct_entry -> inline -> module_path + Id.t -> module_struct_entry -> inline -> module_path val add_include : module_struct_entry -> bool -> inline -> delta_resolver @@ -65,16 +65,16 @@ val set_engagement : engagement -> unit (** [start_*] functions return the [module_path] valid for components of the started module / module type *) -val start_module : identifier -> module_path +val start_module : Id.t -> module_path -val end_module : Summary.frozen ->identifier -> +val end_module : Summary.frozen ->Id.t -> (module_struct_entry * inline) option -> module_path * delta_resolver val add_module_parameter : mod_bound_id -> module_struct_entry -> inline -> delta_resolver -val start_modtype : identifier -> module_path -val end_modtype : Summary.frozen -> identifier -> module_path +val start_modtype : Id.t -> module_path +val end_modtype : Summary.frozen -> Id.t -> module_path val pack_module : unit -> module_body |