Demodulate used to be a reduction_kind and it used to take a ~pattern.

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

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index ccff1fab1d3560cd46e2f2a4d3927259418ae747..f99573b30ccf3840f3444f8c509e1b98a751efc0 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -68,8 +68,7 @@ EXTEND
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
   reduction_kind: [
-    [ IDENT "demodulate" -> `Demodulate
-    | IDENT "normalize" -> `Normalize
+    [ IDENT "normalize" -> `Normalize
     | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
@@ -154,6 +153,7 @@ EXTEND
        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)
+    | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "discriminate"; t = tactic_term ->
         GrafiteAst.Discriminate (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;