New syntax -H1 .. Hn for clear

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 173912e1f1a918586dcf03f45580707ccca8f935..32a29c2158a98e8f1dda73f10191a6a6f6fe3d54 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -41,6 +41,7 @@ type ntactic =
    | NCases of loc * NotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * NotationPt.term
+   | NClear of loc * string list
    | NConstructor of loc * int option * NotationPt.term list
    | NCut of loc * NotationPt.term
 (* | NDiscriminate of loc * NotationPt.term
@@ -86,10 +87,6 @@ let magic = 35
 (* composed magic: term + command magics. No need to change this value *)
 let magic = magic + 10000 * NotationPt.magic
 
-type command =
-  | Set of loc * string * string
-  | Print of loc * string
-
 type alias_spec =
   | Ident_alias of string * string        (* identifier, uri *)
   | Symbol_alias of string * int * string (* name, instance no, description *)
@@ -97,7 +94,7 @@ type alias_spec =
 
 type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
 
-type ncommand =
+type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)
   | UnificationHint of loc * NotationPt.term * int (* term, precedence *)
   | NObj of loc * NotationPt.term NotationPt.obj
@@ -121,8 +118,7 @@ type ncommand =
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
 type code =
-  | Command of loc * command
-  | NCommand of loc * ncommand
+  | NCommand of loc * command
   | NMacro of loc * nmacro 
   | NTactic of loc * ntactic list