Commit e9a6fd45 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

remove debug output in eliminate_definition

parent 10b5e6c6
...@@ -31,11 +31,7 @@ let add_t_ax task nm ls hd e = ...@@ -31,11 +31,7 @@ let add_t_ax task nm ls hd e =
let vl = Svs.elements (t_freevars Svs.empty hd) in let vl = Svs.elements (t_freevars Svs.empty hd) in
let ax = f_forall vl [[Term hd]] (f_equ hd e) in let ax = f_forall vl [[Term hd]] (f_equ hd e) in
let id = id_derive (nm ^ "_def") ls.ls_name in let id = id_derive (nm ^ "_def") ls.ls_name in
try
add_decl task (create_prop_decl Paxiom (create_prsymbol id) ax) add_decl task (create_prop_decl Paxiom (create_prsymbol id) ax)
with
UnboundVars vs ->
Format.printf "@[%a@\n@]" Pretty.print_fmla ax; assert false
let add_f_ax task nm ls hd e = let add_f_ax task nm ls hd e =
let vl = Svs.elements (f_freevars Svs.empty hd) in let vl = Svs.elements (f_freevars Svs.empty hd) 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