From 5d2d801149383671c5ed9ed98fa5e85cc86a63fc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 20 May 2006 10:49:11 +0000 Subject: [PATCH 1/1] commented out a line to help paramodulation. now if 0 goals are open every tactic is vacuosly performed --- helm/software/components/tactics/continuationals.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml index 3ed167a71..4c00fd704 100644 --- a/helm/software/components/tactics/continuationals.ml +++ b/helm/software/components/tactics/continuationals.ml @@ -270,7 +270,13 @@ struct match cmd, stack with | _, [] -> assert false | Tactical tac, (g, t, k, tag) :: s -> - if g = [] then fail (lazy "can't apply a tactic to zero goals"); +(* COMMENTED OUT TO ALLOW PARAMODULATION TO DO A + * auto paramodulation.try assumption. + * EVEN IF NO GOALS ARE LEFT OPEN BY AUTO. + + if g = [] then fail (lazy "can't apply a tactic to zero goals"); + +*) debug_print (lazy ("context length " ^string_of_int (List.length g))); let rec aux s go gc = function -- 2.39.2