X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4;hb=fa3139698294b99889afd375298f9b071cdfbd67;hp=e251ae557dcc25ca119c4f870966fd27b32d428e;hpb=70aa6dc959dc1d49f751c183367c3b73393c938b;p=helm.git

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e251ae557..1175d3cc1 100644
--- 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
@@ -91,7 +92,7 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *)
+type inclusion_mode = WithPreferences | WithoutPreferences | OnlyPreferences (* aka aliases *)
 
 type command =
   | Include of loc * inclusion_mode * string (* _,buri,_,path *)