From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 27 Mar 2009 12:12:50 +0000 (+0000)
Subject: more comments
X-Git-Tag: make_still_working~4134
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=765189dfcb70fc21d14c4fdf80b6f0e0c311ee56;p=helm.git

more comments
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index baa7f38a9..b7d06031b 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -180,6 +180,8 @@ let compare_menv ~past ~present =
     1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
     2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
          distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
+    3) tac G = distribute_tac (exec tac) G if  
+       tac = distribute_tac lowtac
 
    Note that executing an high tactic on a set of goals may be stronger
    than executing the same tactic on those goals, but once at a time