From 5357e090aa81403bd99bb56a023a5d46d34d92f0 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. --- helm/software/components/cic_unification/cicRefine.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 4b310ef75..7f5ab6883 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/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