From 061ed2c930ca832db175a0bc85351c98819d6bda Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Jun 2000 13:35:13 +0000
Subject: Doc

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

(limited to 'kernel')

diff --git a/kernel/generic.mli b/kernel/generic.mli
index 4f2afa9a0f..3f14efaee1 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -49,6 +49,9 @@ val pop : 'a term -> 'a term
    more recent terms come first in [ctxt] *)
 val lift_context : int -> (name * 'a term) list -> (name * 'a term) list
 
+(* [substnl [a1;...;an] k c] substitutes in parallele [a1],...,[an]
+    for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
+    accordingly indexes in [a1],...,[an] *)
 val substnl : 'a term list -> int -> 'a term -> 'a term
 val substl : 'a term list -> 'a term -> 'a term
 val subst1 : 'a term -> 'a term -> 'a term
-- 
cgit v1.2.3