Commit 57259417 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Using t_replace modulo attributes in generalize introduced.

parent a5596d5b
......@@ -190,6 +190,15 @@ let () = Trans.register_transform "introduce_premises" introduce_premises
~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
goal@ into@ constant@ symbol@ and@ axioms."
(* In this file t_replace is used to substitute vsymbol with lsymbols. This is
done in [set_vs]; but in cases where the attribute is directly on the lsymbol
term application (Tapp), the substitution may not work resulting in an error
of the transformation. That's why we check for equality modulo attributes and
then copy attributes back on the term again.
let rec t_replace t1 t2 t =
if t_equal_nt_na t t1 then t_attr_copy t t2 else t_map (t_replace t1 t2) t
let rec generalize hd =
match hd.Task.task_decl.Theory.td_node with
| Theory.Decl {d_node = Dprop (Pgoal,pr,f)} ->
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