X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=553e1e6716654ebcc9a62de0c6d561b69b2bbdb5;hb=6b76c5b3b82753966cabffd8536d8dd9f8cada20;hp=7d8a45d0e6d9b660ca9f618e7dc25e7b3e858a24;hpb=aa5c8c99c9f7ae285883cff133fc02b3d064888c;p=helm.git

diff --git a/matita/components/ng_refiner/nCicUnification.ml b/matita/components/ng_refiner/nCicUnification.ml
index 7d8a45d0e..553e1e671 100644
--- a/matita/components/ng_refiner/nCicUnification.ml
+++ b/matita/components/ng_refiner/nCicUnification.ml
@@ -19,7 +19,7 @@ exception KeepReducingThis of
   string Lazy.t * (NCicReduction.machine * bool) * 
                   (NCicReduction.machine * bool) ;;
 
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
 
 let mk_msg (status:#NCic.status) metasenv subst context t1 t2 =
  (lazy (