From 8a74607bfb8c49e529c4b55a8cad92dd0c68012f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 11 Jun 2012 08:29:15 +0000 Subject: [PATCH] New nohyps option for /demod/ --- matita/components/grafite_parser/grafiteParser.ml | 1 + 1 file changed, 1 insertion(+) 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: [ -- 2.39.2