X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fnat_fact%2Ftimes.ma;h=88e2602b886f79f5023750ae9de76578934ba164;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=43c213c9b3f00b6de8e38f13f98efb7a324598bf;hpb=7a116453d799657958e32693be28d18a5aab84fc;p=helm.git

diff --git a/helm/software/matita/library/Q/nat_fact/times.ma b/helm/software/matita/library/Q/nat_fact/times.ma
index 43c213c9b..88e2602b8 100644
--- a/helm/software/matita/library/Q/nat_fact/times.ma
+++ b/helm/software/matita/library/Q/nat_fact/times.ma
@@ -30,7 +30,7 @@ let rec times_f h g \def
 theorem eq_times_f_times1:\forall g,h,m. defactorize_aux (times_f g h) m
 =defactorize_aux g m*defactorize_aux h m.
 intro.elim g
-  [elim h;simplify;autobatch
+  [elim h;simplify;autobatch;
   |elim h
     [simplify;autobatch
     |simplify.rewrite > (H n3 (S m)).autobatch