bugfix update in basic_2

[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..52cdb3840c371ed2776f9b879a5f419110d11ae8 100644 (file)
--- a/matita/components/ng_kernel/nCicReduction.ml
+++ b/matita/components/ng_kernel/nCicReduction.ml
@@ -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
 ;;