X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicDischarge.ml;h=65b5cea3393918525b68a721f7713b39955f32a0;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=f5bcee20b761c0b1547e43f06b86ab74da2f4c86;hpb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicDischarge.ml b/helm/software/components/cic_proof_checking/cicDischarge.ml
index f5bcee20b..65b5cea33 100644
--- 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 "D 1" lpsno args in
+	          let largs, _ = X.split_nth lpsno args in
 		  C.Appl (hd :: largs @ Ut.mk_rels rpsno 0)  
 	       | _                                                     ->
 	          assert false