]> matita.cs.unibo.it Git - helm.git/commitdiff
added Auto parsing
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 3 Nov 2004 14:31:22 +0000 (14:31 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 3 Nov 2004 14:31:22 +0000 (14:31 +0000)
helm/ocaml/cic_disambiguation/cicTextualParser2.ml

index 0c00d869809435ce403d5ce4e5c0130237bc2406..53559bcd298e8cb80a7be1fc7a9cd62d5381fafc 100644 (file)
@@ -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 ->