Commit 906a84ea authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix encoding of constants (for TPTP provers).

Locations and labels were leaking into constant definitions, thus
preventing TPTP provers to unify them when equal. Example:
const_shdqproofssldtdtsltest_harnessdtmlwdq_17_23_24sh_3 <> const_3.
parent c5b6c1f2
......@@ -131,6 +131,7 @@ let ls_of_const =
let ht = Hterm.create 63 in
fun t -> match t.t_node with
| Tconst _ ->
let t = t_label Slab.empty t in
begin try Hterm.find ht t with Not_found ->
let s = "const_" ^ Pp.string_of_wnl Pretty.print_term t in
let ls = create_fsymbol (id_fresh s) [] ty_base 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