X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicRefine.ml;h=b535b9ebe987677505d7d9b40a2c59731a4c2606;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=537290dc6d062af26e090f61d403e2d87c1a3d07;hpb=f49690e1d1b39ccad40f1e874d9d19f6ffc289e0;p=helm.git

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 537290dc6..b535b9ebe 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1553,7 +1553,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true)
                      let get_l_r_p n = function
                        | Cic.Lambda (_,Cic.MutInd _,_) -> [],[]
                        | Cic.Lambda (_,Cic.Appl (Cic.MutInd _ :: args),_) ->
-                           HExtlib.split_nth "R 1" n args
+                           HExtlib.split_nth n args
                        | _ -> assert false
                      in
                      let _, _, ty, cl = List.nth tl tyno in
@@ -1626,7 +1626,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true)
                          (CR.head_beta_reduce ~delta:false 
                           (Cic.Appl [outty;k])))),k
                    | Cic.Appl (Cic.MutInd _::pl) ->
-                       let left_p,right_p = HExtlib.split_nth "R 2" leftno pl in
+                       let left_p,right_p = HExtlib.split_nth leftno pl in
                        let has_rights = right_p <> [] in
                        let k = 
                          let k = Cic.MutConstruct (uri,tyno,i,[]) in
@@ -1638,7 +1638,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true)
                              CicUniv.oblivion_ugraph 
                          with
                          | Cic.Appl (Cic.MutInd _::args),_ ->
-                             snd (HExtlib.split_nth "R 3" leftno args)
+                             snd (HExtlib.split_nth leftno args)
                          | _ -> assert false
                          with CicTypeChecker.TypeCheckerFailure _-> assert false
                        in
@@ -1694,7 +1694,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true)
                    with
                    | (Cic.MutInd _ | Cic.Meta _) as mty,_ -> [], mty
                    | Cic.Appl ((Cic.MutInd _|Cic.Meta _)::args) as mty,_ ->
-                       snd (HExtlib.split_nth "R 4" leftno args), mty
+                       snd (HExtlib.split_nth leftno args), mty
                    | _ -> assert false
                  with CicTypeChecker.TypeCheckerFailure _ -> 
                     raise (AssertFailure(lazy "already ill-typed matched term"))