From 4c116e043436a3bb7fdc19bf0100d662916cea27 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:57:04 +0000 Subject: [PATCH] Ooops. In previous commit I forgot to subtract the left arguments in case analysis. --- components/cic_disambiguation/disambiguate.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml index 6dd82cc28..3d671cd7f 100644 --- a/components/cic_disambiguation/disambiguate.ml +++ b/components/cic_disambiguation/disambiguate.ml @@ -247,7 +247,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ in let branches = match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with - Cic.InductiveDefinition (il,_,_,_) -> + Cic.InductiveDefinition (il,_,leftsno,_) -> let _,_,_,cl = try List.nth il indtype_no @@ -284,7 +284,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~ in let branch,tl = find_and_remove branches in let (_,_,args),_ = branch in - if List.length args = count_prod ty then + if List.length args = count_prod ty - leftsno then branch::sort tl cltl else raise -- 2.39.2