X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FdiscriminationTactics.ml;h=dd122ee4850419326ef50c38afa31022d25e9915;hb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;hp=c9feaaee68da093fd97a49df693886a463fc5931;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml
index c9feaaee6..dd122ee48 100644
--- a/helm/ocaml/tactics/discriminationTactics.ml
+++ b/helm/ocaml/tactics/discriminationTactics.ml
@@ -59,7 +59,7 @@ let rec injection_tac ~term =
                              T.then_ 
                               ~start:(injection1_tac ~i ~term)
                               ~continuation:(traverse_list (i+1) tl1 tl2)
-                          | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac
+                          | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
                        in traverse_list 1 applist1 applist2
                     | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
                        (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))