Revert "Make proof obsolete when shapes are different"

This reverts commit f2886c41.

src/session/termcode.ml

@@ -1106,8 +1106,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;