X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=3a0edb7ac59ee3071166848080dfbc002be163db;hb=d46411c038cccb932638fd9d131c5d858c80ac5e;hp=941bb221871192ae6ecaf32f7d9dcc75fd54dbb9;hpb=c0700c9d9cf3aa044b2f2945a832a6c2eebd5409;p=helm.git

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 941bb2218..3a0edb7ac 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -730,16 +730,6 @@ EXTEND
            if rew = None then G.Hint (loc, false) else G.Hint (loc,true)
       | IDENT "auto"; params = auto_params ->
           G.AutoInteractive (loc,params)
-      | [ IDENT "whelp"; "match" ] ; t = term -> 
-          G.WMatch (loc,t)
-      | [ IDENT "whelp"; IDENT "instance" ] ; t = term -> 
-          G.WInstance (loc,t)
-      | [ IDENT "whelp"; IDENT "locate" ] ; id = QSTRING -> 
-          G.WLocate (loc,id)
-      | [ IDENT "whelp"; IDENT "elim" ] ; t = term ->
-          G.WElim (loc, t)
-      | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
-          G.WHint (loc,t)
       ]
     ];
     alias_spec: [