Merge branch 'declarative' into matita-lablgtk3

[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..7542a52e03683ce1bb3905c3e6dc28fe7b7c2af9 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
@@ -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
 ;;