Big change:

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 32a29c2158a98e8f1dda73f10191a6a6f6fe3d54..1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -92,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 *)