X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=05504f511f3c149913256f7740cffb861b231730;hb=1acfe506c30e7fcc9d6e427d2523130c371a1159;hp=63df8ab7f37d1b6a208e89bd16b599ec67da2512;hpb=06a19bec47845ecffe3bf9d9a95d3d4dadf76861;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 63df8ab7f..05504f511 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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";