From 765189dfcb70fc21d14c4fdf80b6f0e0c311ee56 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Mar 2009 12:12:50 +0000 Subject: [PATCH] more comments --- helm/software/components/ng_tactics/nTactics.ml | 2 ++ 1 file changed, 2 insertions(+) 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 -- 2.39.2