From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 Dec 2009 16:07:57 +0000 (+0000)
Subject: param "slir" to call the new auto
X-Git-Tag: make_still_working~3171
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68b13bbcf487f7575d5f04f6b2c23aa9ef02409b;p=helm.git

param "slir" to call the new auto
and "fast paramod" for the constrained narrowing of the goal
---

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 2914a8906..b35245f90 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -478,6 +478,8 @@ EXTEND
 ];
   auto_fixed_param: [
    [ IDENT "paramodulation"
+   | IDENT "fast_paramod"
+   | IDENT "slir"
    | IDENT "depth"
    | IDENT "width"
    | IDENT "size"