added Auto parsing

[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 0c00d869809435ce403d5ce4e5c0130237bc2406..53559bcd298e8cb80a7be1fc7a9cd62d5381fafc 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -251,6 +251,7 @@ EXTEND
         return_tactic loc (TacticAst.Apply t)
     | [ IDENT "assumption" | IDENT "Assumption" ] ->
         return_tactic loc TacticAst.Assumption
+    | [ IDENT "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
     | [ IDENT "change" | IDENT "Change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->