From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 1 Jun 2011 11:27:34 +0000 (+0000)
Subject: assert false removed
X-Git-Tag: make_still_working~2475
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03c0037e213792cff9cace9b0dd0d93b10bb5ae0;p=helm.git

assert false removed
---

diff --git a/matita/components/ng_kernel/nCicReduction.ml b/matita/components/ng_kernel/nCicReduction.ml
index 8a84810a3..52cdb3840 100644
--- 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
 ;;