diff options
Diffstat (limited to 'kernel/mod_subst.mli')
-rw-r--r-- | kernel/mod_subst.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 5384d0f85..6ae9649d6 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -85,6 +85,8 @@ val occur_mbid : mod_bound_id -> substitution -> bool val update_subst_alias : substitution -> substitution -> substitution +val update_subst : substitution -> substitution -> substitution + val subst_key : substitution -> substitution -> substitution val join_alias : substitution -> substitution -> substitution |