X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=ae4dc23f76b4e477f2276d268b96670bd5decdc2;hb=5ede839a0cf3339568202750b4aae85ccc63fcb0;hp=5b10a5465cc5fc9ad68889fc87a8236ad3bede2c;hpb=a14adba81c00c9dcb9996d7af39e4803214606f1;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 5b10a5465..ae4dc23f7 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -65,6 +65,7 @@ type ntactic =
    | 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
@@ -200,6 +201,8 @@ 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 *)