diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 7503aa03a6..f942fe1787 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -977,11 +977,13 @@ let replace_vars var_alist = let subst_var str = replace_vars [(str, mkRel 1)] (* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *) -let subst_vars vars = +let substn_vars p vars = let _,subst = - List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (1,[]) vars + List.fold_left (fun (n,l) var -> ((n+1),(var,mkRel n)::l)) (p,[]) vars in replace_vars (List.rev subst) +let subst_vars = substn_vars 1 + (*********************) (* Term constructors *) (*********************) @@ -1242,7 +1244,7 @@ let destArity = | IsLetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c | IsCast (c,_) -> prodec_rec l c | IsSort s -> l,s - | _ -> anomaly "decompose_arity: not an arity" + | _ -> anomaly "destArity: not an arity" in prodec_rec [] @@ -1387,16 +1389,6 @@ let global_vars_set constr = in filtrec Idset.empty constr -(* [Rel (n+m);...;Rel(n+1)] *) - -let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) - -let rel_list n m = - let rec reln l p = - if p>m then l else reln (mkRel(n+p)::l) (p+1) - in - reln [] 1 - (* Rem: end of import from old module Generic *) (* Various occurs checks *) |