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

diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 2738b1c90..6b78512bd 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 leftno args)
+      ens,fst (HExtlib.split_nth "ON 1" leftno args)
    | _ -> assert false
  in
   let rec aux n irl context outsort =