From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 08b1e5e863..858ba24655 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -474,9 +474,9 @@ val subst_var : identifier -> constr -> constr
    if two names are identical, the one of least indice is keeped *)
 val subst_vars : identifier list -> constr -> constr
 
-(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *)
-val rel_vect : int -> int -> constr array
-val rel_list : int -> int -> constr list
+(* [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+   if two names are identical, the one of least indice is keeped *)
+val substn_vars : int -> identifier list -> constr -> constr
 
 (*s Compact representation of implicit lifts. \\
    [ELSHFT(l,n)] == lift of [n], then apply [lift l].
-- 
cgit v1.2.3