From 161bf6d64ebcaf53ee1a15f07f33a6ffc93854ef Mon Sep 17 00:00:00 2001
From: coq
Date: Wed, 4 Dec 2002 11:09:01 +0000
Subject: Corrige un bug de composition de substitutions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3372 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index 2ecdd602d8..89c90fef1a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -96,6 +96,9 @@ val add_mbid :
 val map_msid : mod_self_id -> module_path -> substitution
 val map_mbid : mod_bound_id -> module_path -> substitution
 
+(* sequential composition: 
+   [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
+*)
 val join : substitution -> substitution -> substitution
 
 (*i debugging *)
-- 
cgit v1.2.3