diff options
Diffstat (limited to 'kernel/generic.ml')
| -rw-r--r-- | kernel/generic.ml | 10 |
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)] *) |