new intro:

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index faa17124edd09053a0634267af03ae4fdb3acb35..d7aae9ee8c1bc9021686b619ae096943a3d4c4a0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -276,6 +276,7 @@ EXTEND
        | Some `Trace ->
           G.NMacro(loc,
              G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
+    | IDENT "nintros" -> G.NMacro (loc, G.NIntroGuess loc)
     | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
     | IDENT "screenshot"; fname = QSTRING -> 
         G.NMacro(loc,G.Screenshot (loc, fname))
@@ -315,7 +316,7 @@ EXTEND
             (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
         G.NTactic(loc,[G.NBlock (loc,l)])
     | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
-    | SYMBOL "#"; n=IDENT -> G.NTactic(loc,[ G.NIntro (loc,n)])
+    | SYMBOL "#"; ns=LIST0 IDENT -> G.NTactic(loc,[ G.NIntros (loc,ns)])
     | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
     | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
     | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])