From bfd0ee9503cf04b51b2dd40d4ad2a904b07ac323 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 20 Sep 2015 00:06:33 +0200
Subject: Fix #3948 Anomaly: unknown constant in Print Assumptions

Substitution on bound modules was incorrectly extended without sequential
composition.
---
 kernel/mod_subst.ml  | 2 +-
 kernel/mod_subst.mli | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f7ae30e7af..ba14f65d9e 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' =
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
 
-(** Extending a [substitution] *)
+(** Extending a [substitution] without sequential composition *)
 
 let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
 let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fc2b0441ca..cd9fa79216 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 :
-- 
cgit v1.2.3