Porting to ocaml 5

[helm.git] / matita / components / ng_kernel / nCicReduction.ml

diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml
index 8a84810a3cfd456d39b4199ae48f46d054f0793a..9234f07aab85f9acf1d2fc5831b0743f7e7733cc 100644 (file)
--- 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);;
 
@@ -330,7 +330,9 @@ let alpha_eq (status:#NCic.status) ~test_lambda_source aux test_eq_only metasenv
        (is_prop || aux test_eq_only context term1 term2) &&
        (try List.for_all2 (aux test_eq_only context) pl1 pl2
         with Invalid_argument _ -> false)
-   | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+   | (C.Implicit _, _) | (_, C.Implicit _) -> true
+     (* CSC: was assert false, but it happens when looking for coercions
+        during pretty printing of terms yet to be refined *)
    | (_,_) -> false
 ;;