Commit 2c4e68b5 authored by Sylvain Dailler's avatar Sylvain Dailler

fixes #25

We now use equality for terms modulo triggers and labels for replace.
parent 40b25049
......@@ -22,8 +22,11 @@ exception Unnecessary_terms of term list
let gen_ident = Ident.id_fresh
let rec t_replace_nt_nl t1 t2 t =
if t_equal_nt_nl t t1 then t2 else t_map (t_replace_nt_nl t1 t2) t
(* Replace all occurences of f1 by f2 in t *)
let replace_in_term = Term.t_replace
let replace_in_term = t_replace_nt_nl
(* TODO be careful with label copy in t_map *)
let subst_quant c tq x : term =
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