Commit f29d694b authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Revert "Make proof obsolete when shapes are different"

This reverts commit f2886c41.
parent 168fd5c6
......@@ -1105,8 +1105,7 @@ module Pairing (Old: S)(New: S) = struct
let oldi = Hashtbl.find old_checksums c in
let oldg = table.table_old.(oldi) in
Hashtbl.remove old_checksums c;
let obs = Old.shape oldg <> New.shape newg in
result.(new_goal_index newg) <- (newg, Some (oldg, obs))
result.(new_goal_index newg) <- (newg, Some (oldg, false))
with Not_found ->
acc := mk_node table (New newi) :: !acc
done;
......
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