]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_kernel/nCicReduction.ml
Porting to ocaml 5
[helm.git] / matita / components / ng_kernel / nCicReduction.ml
index 52cdb3840c371ed2776f9b879a5f419110d11ae8..9234f07aab85f9acf1d2fc5831b0743f7e7733cc 100644 (file)
@@ -18,7 +18,7 @@ module E = NCicEnvironment
 exception AssertFailure of string Lazy.t;;
 
 let debug = ref false;;
-let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+(*let pp m = if !debug then prerr_endline (Lazy.force m) else ();;*)
 
 module type Strategy = sig
   type stack_term
@@ -206,7 +206,7 @@ module R = Reduction(RS);;
 
 let whd = R.whd
 
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
 
 let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);;