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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/mod_subst.ml')

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
-- 
cgit v1.2.3