PrimitiveTactics: intros _ now aveilable

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 63df8ab7f37d1b6a208e89bd16b599ec67da2512..05504f511f3c149913256f7740cffb861b231730 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -65,7 +65,11 @@ EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
-  ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
+  new_name: [
+    [ id = IDENT -> Some id
+    | SYMBOL "_" -> None ]
+    ];
+  ident_list0: [ [ LPAREN; idents = LIST0 new_name; RPAREN -> idents ] ];
   tactic_term_list1: [
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
@@ -144,8 +148,8 @@ EXTEND
     | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
     | IDENT "cases"; what = tactic_term;
-      (num, idents) = intros_spec ->
-       GrafiteAst.Cases (loc, what, idents)
+      specs = intros_spec ->
+       GrafiteAst.Cases (loc, what, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
@@ -158,7 +162,7 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
@@ -171,10 +175,10 @@ EXTEND
           | None         -> None, [], Some Ast.UserInput
           | Some pattern -> pattern   
        in
-       GrafiteAst.Elim (loc, what, using, pattern, num, idents)
+       GrafiteAst.Elim (loc, what, using, pattern, (num, idents))
     | IDENT "elimType"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
-       GrafiteAst.ElimType (loc, what, using, num, idents)
+       GrafiteAst.ElimType (loc, what, using, (num, idents))
     | IDENT "exact"; t = tactic_term ->
         GrafiteAst.Exact (loc, t)
     | IDENT "exists" ->
@@ -190,17 +194,17 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 new_name -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
        GrafiteAst.Generalize (loc,p,id)
     | IDENT "id" -> GrafiteAst.IdTac loc
     | IDENT "intro"; ident = OPT IDENT ->
-        let idents = match ident with None -> [] | Some id -> [id] in
-        GrafiteAst.Intros (loc, Some 1, idents)
-    | IDENT "intros"; (num, idents) = intros_spec ->
-        GrafiteAst.Intros (loc, num, idents)
+        let idents = match ident with None -> [] | Some id -> [Some id] in
+        GrafiteAst.Intros (loc, (Some 1, idents))
+    | IDENT "intros"; specs = intros_spec ->
+        GrafiteAst.Intros (loc, specs)
     | IDENT "inversion"; t = tactic_term ->
         GrafiteAst.Inversion (loc, t)
     | IDENT "lapply";