- hExtlib: added debugging information for split_nth

[helm.git] / helm / software / components / cic_proof_checking / cicDischarge.ml

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index 65b5cea3393918525b68a721f7713b39955f32a0..f5bcee20b761c0b1547e43f06b86ab74da2f4c86 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicDischarge.ml
+++ b/helm/software/components/cic_proof_checking/cicDischarge.ml
@@ -220,7 +220,7 @@ let rec discharge_term st t = match t with
            let vty = match vty with
               | C.Appl (C.MutInd (fu, fm, _) as hd :: args) 
                  when UM.eq fu u && fm = m && List.length args = psno ->
-                 let largs, _ = X.split_nth lpsno args in
+                 let largs, _ = X.split_nth "D 1" lpsno args in
                  C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)  
               | _                                                     ->
                  assert false