Commit 15aa6034 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Allow rewrite to use iff and to apply on head part of a formula

parent bbb8f44b
......@@ -223,7 +223,7 @@ let replace_subst lp lv f1 f2 withed_terms t =
in
let is_replaced, t =
t_map_fold (fun is_replaced t -> replace is_replaced f1 f2 t) None t in
replace None f1 f2 t in
match is_replaced with
| None -> raise (Arg_trans "rewrite: no term matching the given pattern")
| Some(subst_ty,subst) ->
......@@ -242,6 +242,9 @@ let rewrite_in rev with_terms h h1 =
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Support to rewrite from the right *)
if rev then (t1, t2) else (t2, t1)
| Tbinop (Tiff, t1, t2) ->
(* Support to rewrite from the right *)
if rev then (t1, t2) else (t2, t1)
| _ -> raise (Arg_bad_hypothesis ("rewrite", f))) in
Some (lp, lv, t1, t2)
| _ -> acc) None in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment