Commit e46100ce authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix hash_alpha, removed debug message from gappa printer

parent 5abac257
......@@ -1613,7 +1613,7 @@ let binop_hash = function
let rec t_hash_alpha m t =
match t.t_node with
| Tbvar i -> t_hash_alpha m (bnd_find i m.bv_defer)
| Tbvar i -> 0
| Tvar v -> Hashcons.combine 1 (vs_hash v)
| Tconst c -> Hashcons.combine 2 (Hashtbl.hash c)
| Tapp (s,l) ->
......
......@@ -401,7 +401,9 @@ let print_task env pr thpr ?old:_ fmt task =
(fun f -> Sls.mem f info.info_symbols)
task
in
(*
eprintf "Abstraction: @\n%a@." Pretty.print_task task;
*)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let equations,hyps,goal =
......
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