Small debugging in tptp2grafite

[helm.git] / helm / software / components / tptp_grafite / tptp2grafite.ml

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index ca0534c52b7f3ae410376808cdf63ac9ca4a8dec..009a53a610686a0d352e5dce681f066372abdb79 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -221,7 +221,8 @@ let ng_generate_tactics fv ueq_case context arities =
   (HExtlib.list_mapi
    (fun (name,_) _-> 
      GA.Executable(floc,GA.NTactic(floc, 
-      [GA.NIntro (floc,name);GA.NDot(floc)])))
+      [GA.NIntro (floc,(try List.assoc name kw with Not_found -> name));
+       GA.NDot(floc)])))
    arities)
   @
   (HExtlib.list_mapi
@@ -272,6 +273,8 @@ let ng_generate_tactics fv ueq_case context arities =
                GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
+    [GA.Executable(floc,GA.NTactic(floc,[GA.NTry(floc, GA.NAssumption(floc));
+                                        GA.NSemicolon(floc)]))]@
   [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 ;;