attached 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 a7c7a9ae21329089fc0c3983ca8c6618a08b1a69..34b3d01e0cc18a72dde5f36c0953930b46989681 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -335,7 +335,8 @@ EXTEND
         TacticAst.Apply (loc, t)
     | [ IDENT "assumption" ] ->
         TacticAst.Assumption loc
-    | [ IDENT "auto" ] -> TacticAst.Auto loc
+    | [ IDENT "auto" ] ; num = OPT [ i = NUM -> int_of_string i ] -> 
+          TacticAst.Auto (loc,num)
     | [ IDENT "change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->