X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=3eb64d458fe2892a44f32af5bb1ce5e0af0db1fb;hb=7c84225a8e472e754f1baf8f8b37f8627c8da6fa;hp=dac05d7bdd056d83d146bbef82e03d886efc6742;hpb=63f876b112e1be016e8063e6a00ec47f841ee615;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index dac05d7bd..3eb64d458 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -163,13 +163,14 @@ EXTEND
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)
-    | IDENT "elim"; what = tactic_term; using = using;
+    | IDENT "elim"; what = tactic_term; using = using; 
+       pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->
-	let pattern = Some what, [], Some Ast.UserInput in
-	GrafiteAst.Elim (loc, pattern, using, num, idents)
-    | IDENT "elim"; pattern = pattern_spec; using = using;
-      (num, idents) = intros_spec ->
-	GrafiteAst.Elim (loc, pattern, using, num, idents)    
+	let pattern = match pattern with
+	   | None         -> None, [], Some Ast.UserInput
+	   | Some pattern -> pattern   
+	in
+	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)