perform substitution only if DoesOccur is raised *)
let _,_,term,_ = U.lookup_subst mno subst in
aux (k-s) () (S.subst_meta (0,l) term)
- with U.Subst_not_found _ -> match l with
+ with U.Subst_not_found _ -> () (*match l with
| C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
- | C.Ctx lc -> List.iter (aux (k-s) ()) lc)
+ | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
| t -> U.fold (fun _ k -> k + 1) k aux () t
in
try aux 0 () t; true