]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed in cases (it did not produced the right number of lambdas for the
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Dec 2006 23:23:41 +0000 (23:23 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 20 Dec 2006 23:23:41 +0000 (23:23 +0000)
outtype of dependent inductive types).

components/tactics/primitiveTactics.ml

index 9f9da081830c94da80fdba1bde8df4d3e30e9333..2e9a3db33f9204afa1ab3ccccb19a96f43f06af0 100644 (file)
@@ -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)