X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=590b482c716db80b74b83429aa4808fbb804aa38;hb=cd602bc57c4ceba6188b4cac0dbf5dad8f5df7b6;hp=0f06351b4d8301e7f99cbb41b6731b0272bf2cb4;hpb=a9af753c66a80cb4f50f32e63272f3830cba306c;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 0f06351b4..590b482c7 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -287,7 +287,7 @@ let discriminate'_tac ~term =
                     let (proof',goals') = 
 		     ProofEngineTypes.apply_tactic 
                       (EliminationTactics.elim_type_tac 
-                       ~term:(C.MutInd(LibraryObjects.false_URI (),0,[])))
+                       (C.MutInd(LibraryObjects.false_URI (),0,[])))
                       status 
                     in
                      (match goals' with