From c2ed1f971183c37feeb2f6e757f55330944f0639 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 20 Dec 2006 23:23:41 +0000 Subject: [PATCH] Bug fixed in cases (it did not produced the right number of lambdas for the outtype of dependent inductive types). --- helm/software/components/tactics/primitiveTactics.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 9f9da0818..2e9a3db33 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -581,10 +581,10 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam (uri,exp_named_subst,typeno,args) | _ -> raise NotAnInductiveTypeToEliminate in - let paramsno,patterns = + let paramsno,itty,patterns = match CicEnvironment.get_obj CicUniv.empty_ugraph uri with C.InductiveDefinition (tys,_,paramsno,_),_ -> - let _,_,_,cl = List.nth tys typeno in + let _,_,itty,cl = List.nth tys typeno in let rec aux n context t = match n,CicReduction.whd context t with 0,C.Prod (name,source,target) -> @@ -605,7 +605,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam | 0,_ -> C.Implicit None | _,_ -> assert false in - paramsno, + paramsno,itty, List.map (function (_,cty) -> aux paramsno context cty) cl | _ -> assert false in @@ -623,7 +623,7 @@ let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_nam 0 -> target | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1)) in - add_lambdas paramsno + add_lambdas (count_prods context itty - paramsno) in let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) -- 2.39.2