X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteParser.ml;h=cceeaf10dfb4b717f82e59c6e1d3154221607255;hb=f13efc1fff944ff0d3bd1414eae1739fead31856;hp=908ad007f79cc5fd8a863c09e7dfe84e9f0c9a7f;hpb=2817260358878e72fa359c6d2431b4c7c358a841;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 908ad007f..cceeaf10d 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -125,8 +125,13 @@ EXTEND
         GrafiteAst.Cut (loc, ident, t)
     | IDENT "decide"; IDENT "equality" ->
         GrafiteAst.DecideEquality loc
-    | IDENT "decompose"; where = tactic_term ->
-        GrafiteAst.Decompose (loc, where)
+    | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
+      OPT "names"; num = OPT [num = int -> num];
+      idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in   
+        let types = match types with None -> [] | Some types -> types in
+	let to_spec id = GrafiteAst.Ident id in
+	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "discriminate"; t = tactic_term ->
         GrafiteAst.Discriminate (loc, t)
     | IDENT "elim"; what = tactic_term;