Bug fixed in cases (it did not produced the right number of lambdas for the

outtype of dependent inductive types).

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 9f9da081830c94da80fdba1bde8df4d3e30e9333..2e9a3db33f9204afa1ab3ccccb19a96f43f06af0 100644 (file)
--- 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)