X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=fd757d141a9334ead4539e6c5d74bf0ffc552170;hb=d769719c7c60089f1623d7c31db992326b9408e2;hp=64c10b9b47e575db35b37981aa79ffc15c95d3b8;hpb=9642ec8492f2ef54e280e27a40c2936a02c252f9;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 64c10b9b4..fd757d141 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -157,12 +157,9 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
-        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
-        let types = match types with None -> [] | Some types -> types in
+    | IDENT "decompose"; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
 	let idents = match idents with None -> [] | Some idents -> idents in
-	let to_spec id = GrafiteAst.Ident id in
-	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+	GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "destruct"; t = tactic_term ->
         GrafiteAst.Destruct (loc, t)