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

1 files changed, 7 insertions, 3 deletions

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)] *)