X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=9ea33c2de294acd90212ef37c0fb830000f1324e;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=0cfdef148ced4dfbae84f8d5f0199516cc86e7a3;hpb=da5dd88bbcc43d9f4342e47c922b820abf91c92f;p=helm.git diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 0cfdef148..9ea33c2de 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -43,7 +43,7 @@ type 'lazy_term reduction = type 'ident intros_spec = int option * 'ident option list -type 'term auto_params = 'term list * (string*string) list +type 'term auto_params = 'term list option * (string*string) list type 'term just = [ `Term of 'term @@ -51,16 +51,22 @@ type 'term just = type ntactic = | NApply of loc * CicNotationPt.term + | NSmartApply of loc * CicNotationPt.term | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list | NCases of loc * CicNotationPt.term * npattern | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term | NConstructor of loc * int option * CicNotationPt.term list | NCut of loc * CicNotationPt.term +(* | NDiscriminate of loc * CicNotationPt.term + | NSubst of loc * CicNotationPt.term *) + | NDestruct of loc * string list option * string list | NElim of loc * CicNotationPt.term * npattern | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string + | NIntros of loc * string list + | NInversion of loc * CicNotationPt.term * npattern | NLApply of loc * CicNotationPt.term | NLetIn of loc * npattern * CicNotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern @@ -71,6 +77,7 @@ type ntactic = | NBranch of loc | NShift of loc | NPos of loc * int list + | NPosbyname of loc * string | NWildcard of loc | NMerge of loc | NSkip of loc @@ -194,10 +201,12 @@ type ('term,'lazy_term) macro = type nmacro = | NCheck of loc * CicNotationPt.term | Screenshot of loc * string + | NAutoInteractive of loc * CicNotationPt.term auto_params + | NIntroGuess of loc (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 30 +let magic = 34 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -220,6 +229,7 @@ type ('term,'obj) command = type ncommand = | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | NObj of loc * CicNotationPt.term CicNotationPt.obj + | NDiscriminator of loc * CicNotationPt.term | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option | NUnivConstraint of loc * NUri.uri * NUri.uri | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list