more comments

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index baa7f38a99bd78d72fc751822842b164a1a5731b..b7d06031bd73bf78b338123fbe04f6f6dbc95953 100644 (file)
--- 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