X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=1175d3cc131c7fc9a6083f5ea072c59ad4c1fef4;hb=fa3139698294b99889afd375298f9b071cdfbd67;hp=32a29c2158a98e8f1dda73f10191a6a6f6fe3d54;hpb=3a5ad4a99fd7f312424200a9241ea1a4ce7fcd29;p=helm.git diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 32a29c215..1175d3cc1 100644 --- 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 *)