symmetry of equality NOT used in auto

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 775f13f7d7e0f8803baa7f1a58f9408fd17cc8fa..fddf27e9995a100f72df291fcc478def9cf601fd 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -240,9 +240,9 @@ EXTEND
     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
   reduction_kind: [
-    [ "reduce" -> `Reduce
-    | "simpl" -> `Simpl
-    | "whd" -> `Whd ]
+    [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
+    | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
+    | [ IDENT "whd" | IDENT "Whd" ] -> `Whd ]
   ];
   tactic: [
     [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
@@ -296,7 +296,20 @@ EXTEND
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
         return_tactic loc (TacticAst.LetIn (t, where))
-    (* TODO Reduce *)
+    | kind = reduction_kind;
+      pat = OPT [
+        "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+          pat
+      ];
+      terms = LIST0 term SEP SYMBOL "," ->
+        let tac =
+          (match (pat, terms) with
+          | None, [] -> TacticAst.Reduce (kind, None)
+          | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+          | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+          | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+        in
+        return_tactic loc tac
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
         return_tactic loc TacticAst.Reflexivity
     | [ IDENT "replace" | IDENT "Replace" ];