X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=131ccad07004f208153e2742d6d7e4a4c002aa32;hb=HEAD;hp=52cdb3840c371ed2776f9b879a5f419110d11ae8;hpb=03c0037e213792cff9cace9b0dd0d93b10bb5ae0;p=helm.git

diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml
index 52cdb3840..131ccad07 100644
--- a/matita/components/ng_kernel/nCicReduction.ml
+++ b/matita/components/ng_kernel/nCicReduction.ml
@@ -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);;
 
@@ -373,7 +373,7 @@ let are_convertible status ~metasenv ~subst =
         R.reduce status ~delta ~subst context m2
      in
      let rec convert_machines test_eq_only
-       ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2) 
+       (((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2), norm2 as m2))
      =
        (alpha_eq status test_eq_only
          (R.unwind status (k1,e1,t1,[])) (R.unwind status (k2,e2,t2,[])) &&