From ea59394577e54aa491404439f1116410b4f78d2a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:41:20 +0000 Subject: [PATCH] Bug fixed: a MutCase considering a wrong number of cases was not detected. --- components/cic_unification/cicRefine.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index 4b310ef75..7f5ab6883 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -527,6 +527,10 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in + if List.length constructors <> List.length pl then + enrich localization_tbl t + (RefineFailure + (lazy "Wrong number of cases")) ; let rec count_prod t = match CicReduction.whd ~subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) -- 2.39.2