;;
let compare x y =
- (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 *)
- if x = y then 0
+ if NCicReduction.alpha_eq [] [] [] x y then 0
+ (* if x = y then 0 *)
else compare x y
;;
let is_eq = function
| Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt ->
- Some (ty,l,r)
+ Some (ty,l,r)
+(*
| Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r]
when eq equivalence_relation eqt && eq setoid_eq eqt2 ->
- Some (ty,l,r)
+ Some (ty,l,r) *)
| _ -> None
let pp t =