- parser: "whelp ...Â"removed

[helm.git] / matita / components / grafite / grafiteAst.ml

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 9ea33c2de294acd90212ef37c0fb830000f1324e..5adc2e91bb03fbd3efe04fe5dc9b27219a502d6d 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -184,12 +184,6 @@ type inline_param = IPPrefix of string         (* undocumented *)
                   | IPCR                       (* detect convertible rewriting *)
 
 type ('term,'lazy_term) macro = 
-  (* Whelp's stuff *)
-  | WHint of loc * 'term
-  | WMatch of loc * 'term 
-  | WInstance of loc * 'term 
-  | WLocate of loc * string
-  | WElim of loc * 'term
   (* real macros *)
   | Eval of loc * 'lazy_term reduction * 'term
   | Check of loc * 'term