X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FoCic2NCic.ml;h=2738b1c901835183078c7a24b0f3470475f13f02;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=6b78512bd6f9203f29f6405690cdca6dfb655b34;hpb=f49690e1d1b39ccad40f1e874d9d19f6ffc289e0;p=helm.git

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 6b78512bd..2738b1c90 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -258,7 +258,7 @@ prerr_endline ("LEFTNO: " ^ string_of_int leftno ^ "  " ^ CicPp.ppterm arity);*)
   match CicReduction.whd context tty with
      Cic.MutInd (_,_,ens) -> ens,[]
    | Cic.Appl (Cic.MutInd (_,_,ens)::args) ->
-      ens,fst (HExtlib.split_nth "ON 1" leftno args)
+      ens,fst (HExtlib.split_nth leftno args)
    | _ -> assert false
  in
   let rec aux n irl context outsort =