From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

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

(limited to 'kernel/generic.ml')

diff --git a/kernel/generic.ml b/kernel/generic.ml
index 70acca45dd..e7e1acc2f7 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -304,10 +304,14 @@ let replace_vars var_alist =
   in 
   if var_alist = [] then (function x -> x) else substrec 0
 
-let subst_varn str n = replace_vars [(str, (Rel n))]
-
 (* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
-let subst_var str = subst_varn str 1
+let subst_var str = replace_vars [(str, Rel 1)]
+
+(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+let subst_vars vars =
+  let _,subst =
+    List.fold_left (fun (n,l) var -> ((n+1),(var,Rel n)::l)) (1,[]) vars
+  in replace_vars (List.rev subst)
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 
-- 
cgit v1.2.3