- parser: "whelp ...Â"removed

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 941bb221871192ae6ecaf32f7d9dcc75fd54dbb9..3a0edb7ac59ee3071166848080dfbc002be163db 100644 (file)
--- 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: [