X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=590b482c716db80b74b83429aa4808fbb804aa38;hb=08791e80816548121e81e04d3ead8c9a5171d033;hp=76b7337349bcc1dcec2d0e3850282704ba08ceb4;hpb=249d79bebff886846fbab65cc079623d90684baf;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index 76b733734..590b482c7 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -204,7 +204,6 @@ 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