lift_from 1 n t
;;
-let subst arg =
+(* subst t1 t2 *)
+(* substitutes [t1] for [Rel 1] in [t2] *)
+(* if avoid_beta_redexes is true (default: false) no new beta redexes *)
+(* are generated. WARNING: the substitution can diverge when t2 is not *)
+(* well typed and avoid_beta_redexes is true. *)
+let rec subst ?(avoid_beta_redexes=false) arg =
let rec substaux k =
let module C = Cic in
function
begin
match substaux k he with
C.Appl l -> C.Appl (l@tl')
+ (* Experimental *)
+ | C.Lambda (_,_,bo) when avoid_beta_redexes ->
+ (match tl' with
+ [] -> assert false
+ | [he] -> subst ~avoid_beta_redexes he bo
+ | he::tl -> C.Appl (subst he bo::tl))
| _ as he' -> C.Appl (he'::tl')
end
| C.Appl _ -> assert false