type t = NCic.term
- let eq x y = NCicReduction.alpha_eq C.metasenv C.subst C.context x y;;
+ let eq x y = x = y;;
+ (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *)
let rec compare x y =
match x,y with
;;
let compare x y =
- if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0
+ (* if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 *)
+ if x = y then 0
else compare x y
;;