From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:19:53 +0000 (+0000)
Subject: New option "demod" for auto.
X-Git-Tag: make_still_working~2994
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50d12d683b3f1fb9739b1308ca7f328e3e382f1b;hp=9b27b913b9084226d0af5306562d0a1c5ccdaaf7;p=helm.git

New option "demod" for auto.
---

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ef354789a..74991bcb9 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -484,6 +484,7 @@ EXTEND
 ];
   auto_fixed_param: [
    [ IDENT "paramodulation"
+   | IDENT "demod"
    | IDENT "fast_paramod"
    | IDENT "paramod"
    | IDENT "slir"