X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=5d138bbe06624ed27896cfb0511767ee045448a6;hb=d51f9674886d1e609a6ea792b65871dcde4f6503;hp=02e16178077eb412b751b3f7bd63903d8702309e;hpb=f5b9e1d5511a13ca5bb424c149781087aa0c8e31;p=helm.git diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 02e161780..5d138bbe0 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -84,7 +84,7 @@ type nmacro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 36 +let magic = 37 (* composed magic: term + command magics. No need to change this value *) let magic = magic + 10000 * NotationPt.magic @@ -102,7 +102,7 @@ type command = | NObj of loc * nterm NotationPt.obj * bool | NDiscriminator of loc * nterm | NInverter of loc * string * nterm * bool list option * nterm option - | NUnivConstraint of loc * NUri.uri * NUri.uri + | NUnivConstraint of loc * bool * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list | NCoercion of loc * string * bool * (nterm * nterm * (string * nterm) * nterm) option