From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:57:04 +0000 (+0000) Subject: Ooops. In previous commit I forgot to subtract the left arguments in case X-Git-Tag: 0.4.95@7852~99 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c116e043436a3bb7fdc19bf0100d662916cea27;p=helm.git Ooops. In previous commit I forgot to subtract the left arguments in case analysis. --- 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