diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
| commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
| tree | aefad2e3de35f75c46729f9310d33b56d3821961 /kernel/mod_subst.mli | |
| parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
| parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index fc2b0441..cd9fa792 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -68,8 +68,9 @@ val empty_subst : substitution val is_empty_subst : substitution -> bool -(** add_* add [arg2/arg1]\{arg3\} to the substitution with no - sequential composition *) +(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential + composition. Most often this is not what you want. For sequential + composition, try [join (map_mbid mp delta) subs] **) val add_mbid : MBId.t -> module_path -> delta_resolver -> substitution -> substitution val add_mp : |