+ | 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 C.metasenv C.subst C.context x y then 0 *)
+ if x = y then 0
+ else compare x y