]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAst.ml
attached auto
[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml
index d4e94b28bea16ce511ca4341b6489378becedde4..23a8b8e6755c34071a78bdd1419a9ea5e6118808 100644 (file)
@@ -38,7 +38,7 @@ type loc = CicAst.location
 type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | Auto of loc
+  | Auto of loc * int option
   | Assumption of loc
   | Change of loc * 'term * 'term * 'ident option (* what, with what, where *)
   | Change_pattern of loc * 'term pattern * 'term * 'ident option