aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_subst.mli')
-rw-r--r--kernel/mod_subst.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 21b6bf93b..f3c490652 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -62,13 +62,13 @@ val is_empty_subst : substitution -> bool
(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
sequential composition *)
val add_mbid :
- mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution
+ MBId.t -> module_path -> delta_resolver -> substitution -> substitution
val add_mp :
module_path -> module_path -> delta_resolver -> substitution -> substitution
(** map_* create a new substitution [arg2/arg1]\{arg3\} *)
val map_mbid :
- mod_bound_id -> module_path -> delta_resolver -> substitution
+ MBId.t -> module_path -> delta_resolver -> substitution
val map_mp :
module_path -> module_path -> delta_resolver -> substitution
@@ -136,7 +136,7 @@ val subst_mps : substitution -> constr -> constr
(** [occur_*id id sub] returns true iff [id] occurs in [sub]
on either side *)
-val occur_mbid : mod_bound_id -> substitution -> bool
+val occur_mbid : MBId.t -> substitution -> bool
(** [repr_substituted r] dumps the representation of a substituted:
- [None, a] when r is a value