From 7bbe9c8a9fcc471920c18a12fb5745828f2fd188 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Sep 2006 10:23:29 +0000 Subject: [PATCH] Bug fixed in pretty printing in new syntax of MutCases on inductive types with left parameters. --- helm/software/components/cic_proof_checking/cicPp.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml index 136e9ddae..f3560cc3a 100644 --- a/helm/software/components/cic_proof_checking/cicPp.ml +++ b/helm/software/components/cic_proof_checking/cicPp.ml @@ -139,18 +139,20 @@ let rec pp t l = | C.MutCase (uri,n1,ty,te,patterns) -> let connames_and_argsno = (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with - C.InductiveDefinition (dl,_,_,_) -> + C.InductiveDefinition (dl,_,paramsno,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in List.map (fun id,ty -> (* this is just an approximation since we do not have reduction yet! *) - let rec count_prods = + let rec count_prods toskip = function - C.Prod (_,_,bo) -> 1 + count_prods bo + C.Prod (_,_,bo) when toskip > 0 -> + count_prods (toskip - 1) bo + | C.Prod (_,_,bo) -> 1 + count_prods 0 bo | _ -> 0 in - id, count_prods ty + id, count_prods paramsno ty ) cons | _ -> raise CicPpInternalError ) -- 2.39.2