1. rewrite_* and rewrite_back_* merged into one function

[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 fc46cc725e8626ee62f5b0bf0bd949ee4386cc7a..9f6476d281981b3a2970f7e7fe1b417da49aa742 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -351,10 +351,8 @@ EXTEND
           wanted, hyp_paths, goal_path ]
   ];
   direction: [
-    [ IDENT "left" -> `Left
-    | SYMBOL ">" -> `Left
-    | IDENT "right" -> `Right
-    | SYMBOL "<" -> `Right ]
+    [ SYMBOL ">" -> `LeftToRight
+    | SYMBOL "<" -> `RightToLeft ]
   ];
   tactic: [
     [ IDENT "absurd"; t = tactic_term ->