From 03c0037e213792cff9cace9b0dd0d93b10bb5ae0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 1 Jun 2011 11:27:34 +0000 Subject: [PATCH] assert false removed --- matita/components/ng_kernel/nCicReduction.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 ;; -- 2.39.2