From 50d12d683b3f1fb9739b1308ca7f328e3e382f1b Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:19:53 +0000
Subject: [PATCH 1/1] New option "demod" for auto.

---
 helm/software/components/grafite_parser/grafiteParser.ml | 1 +
 1 file changed, 1 insertion(+)

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"
-- 
2.39.2