the decompose tactic is now working

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 908ad007f79cc5fd8a863c09e7dfe84e9f0c9a7f..cceeaf10dfb4b717f82e59c6e1d3154221607255 100644 (file)
--- 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;