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

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 97dbb0486..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
@@ -201,6 +202,7 @@ 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 *)