1) grafiteWalker removed

[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 7950ca15d4e25e329ef2f3f331c6b2b082b5a7c0..ca0534c52b7f3ae410376808cdf63ac9ca4a8dec 100644 (file)
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -272,7 +272,7 @@ let ng_generate_tactics fv ueq_case context arities =
                GA.NSkip floc; GA.NMerge floc]))])
       fv)) 
  else [])@
-  [GA.Executable(floc,GA.Command(floc, GA.NQed(floc)))]
+  [GA.Executable(floc,GA.NCommand(floc, GA.NQed(floc)))]
 ;;
 
 let generate_tactics fv ueq_case =