X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=e60bf7e504264c51ef5802f3f4d8057940aa715a;hb=6b76c5b3b82753966cabffd8536d8dd9f8cada20;hp=5df06d28d001cdfbc0d74a84e15fbbc2f5f1b91c;hpb=aa5c8c99c9f7ae285883cff133fc02b3d064888c;p=helm.git diff --git a/matita/components/ng_kernel/nCicUntrusted.ml b/matita/components/ng_kernel/nCicUntrusted.ml index 5df06d28d..e60bf7e50 100644 --- a/matita/components/ng_kernel/nCicUntrusted.ml +++ b/matita/components/ng_kernel/nCicUntrusted.ml @@ -69,7 +69,7 @@ let metas_of_term status subst context term = List.fold_left (aux ctx) (i::acc) l) | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t in - HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term)) + HExtlib.list_uniq (List.sort Stdlib.compare (aux context [] term)) ;; module NCicHash = @@ -282,7 +282,7 @@ let max_kind k1 k2 = module OT = struct type t = int * NCic.conjecture - let compare (i,_) (j,_) = Pervasives.compare i j + let compare (i,_) (j,_) = Stdlib.compare i j end module MS = HTopoSort.Make(OT)