]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_refiner/nCicUnification.ml
Porting to ocaml 5
[helm.git] / matita / components / ng_refiner / nCicUnification.ml
index 7d8a45d0e6d9b660ca9f618e7dc25e7b3e858a24..553e1e6716654ebcc9a62de0c6d561b69b2bbdb5 100644 (file)
@@ -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 (