X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=9ea33c2de294acd90212ef37c0fb830000f1324e;hb=c76b5031700d8a06d19afb54abc81bf5d34d8242;hp=1d3b21392045d561ef21f7c59050790f6194e5ec;hpb=a82bb964ad0bf0969dae008a4de854532846e455;p=helm.git diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 1d3b21392..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,15 +51,23 @@ 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 + | 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 | NRewrite of loc * direction * CicNotationPt.term * npattern @@ -69,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 @@ -191,10 +200,13 @@ 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 = 27 +let magic = 34 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) @@ -217,7 +229,9 @@ type ('term,'obj) command = type ncommand = | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *) | NObj of loc * CicNotationPt.term CicNotationPt.obj - | NUnivConstraint of loc * bool * NUri.uri * NUri.uri + | 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 | NCoercion of loc * string * CicNotationPt.term * CicNotationPt.term *