From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 11 Jun 2012 08:29:15 +0000 (+0000)
Subject: New nohyps option for /demod/
X-Git-Tag: make_still_working~1642
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8a74607bfb8c49e529c4b55a8cad92dd0c68012f;p=helm.git

New nohyps option for /demod/
---

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 376d9900c..024d321b4 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -253,6 +253,7 @@ EXTEND
    | IDENT "paramod"
    | IDENT "width"
    | IDENT "size"
+   | IDENT "nohyps"
    ]
 ];
   auto_params: [