procedural : some improvements.

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index f3dd386a91540b15c729dbf22a0b4c7c25fcaf4a..fd757d141a9334ead4539e6c5d74bf0ffc552170 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -60,10 +60,6 @@ type by_continuation =
  | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
  | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
 
-let out = ref ignore
-
-let set_callback f = out := f
-
 EXTEND
   GLOBAL: term statement;
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
@@ -161,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)
@@ -678,7 +671,6 @@ EXTEND
             (loc,GrafiteAst.Include (iloc,buri))))
     | scom = lexicon_command ; SYMBOL "." ->
        fun ~include_paths status ->
-        !out scom;
        let status = LexiconEngine.eval_command status scom in
          status,LNone loc
     | EOI -> raise End_of_file