diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:06:33 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-09-20 00:14:32 +0200 |
commit | bfd0ee9503cf04b51b2dd40d4ad2a904b07ac323 (patch) | |
tree | 3cc2e5b414ab0b5a8aa00b2023982dc40ae00ca7 /kernel/mod_subst.mli | |
parent | 04e9be59051ca60bf61d5142ac14386920876926 (diff) |
Fix #3948 Anomaly: unknown constant in Print Assumptions
Substitution on bound modules was incorrectly extended without sequential
composition.
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 fc2b0441c..cd9fa7921 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 : |