- | NCic.Rel i, NCic.Rel j -> i-j
- | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2
- | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *)
- | _ -> assert false
+ | NCic.Rel i, NCic.Rel j -> j-i
+ | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j
+ | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2
+ (*NReference.compare r1 r2*)
+ | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2
+ | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1
+ | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1
+ | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
+ | NCic.Appl _, NCic.Meta _ -> ~-1
+ | NCic.Meta _, NCic.Appl _ -> 1
+ | _ -> Pervasives.compare x y
+ (* was assert false, but why? *)
+
+ ;;
+
+ let compare x y =
+ if NCicReduction.alpha_eq [] [] [] x y then 0
+ (* if x = y then 0 *)
+ else compare x y
+ ;;
+
+ let eqP = (!eqPref)()