let is_identity ((metasenv, context, ugraph) as env) = function
| ((_, _, (ty, left, right, _), menv, _) as equality) ->
- (prerr_endline ("left = "^(CicPp.ppterm left));
- prerr_endline ("right = "^(CicPp.ppterm right));
(left = right ||
(* (meta_convertibility left right) || *)
(fst (CicReduction.are_convertible
- ~metasenv:(metasenv @ menv) context left right ugraph))))
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
;;