name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / ocaml / tactics / discriminationTactics.ml

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 0f06351b4d8301e7f99cbb41b6731b0272bf2cb4..76b7337349bcc1dcec2d0e3850282704ba08ceb4 100644 (file)
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -204,6 +204,7 @@ exception TwoDifferentSubtermsFound of int
 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
 diversi *)
 
+(* FG: METTERE I NOMI ANCHE QUI? *)
 let discriminate'_tac ~term =
  let discriminate'_tac ~term status = 
   let (proof, goal) = status in
@@ -287,7 +288,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