X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=3f4d4226f96fe5f19f40cb75495cae1a7707a9a2;hb=d43002dfc61afac676ea14bc6a1418e5ec0e3e9c;hp=48fbc4aa2115d9800e702ba8a1515beb7bbbc93a;hpb=cb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 48fbc4aa2..3f4d4226f 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -38,7 +38,7 @@ type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option (* depth, width *)
+  | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *)
   | Change of loc * ('term,'ident) pattern * 'term
   | Clear of loc * 'ident
   | ClearBody of loc * 'ident