]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/discriminationTactics.ml
changed default parameter values...
[helm.git] / helm / ocaml / tactics / discriminationTactics.ml
index 0f06351b4d8301e7f99cbb41b6731b0272bf2cb4..590b482c716db80b74b83429aa4808fbb804aa38 100644 (file)
@@ -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