now destruct takes an optional list of term rather than a sigle optional term

[helm.git] / components / tactics / autoTypes.mli

diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli
index a026a908fa659fd869d5720673fc9a534e934314..306c42daa75c22c73af7b52a399def3cfac19b67 100644 (file)
--- a/components/tactics/autoTypes.mli
+++ b/components/tactics/autoTypes.mli
@@ -27,6 +27,7 @@ type flags = {
   maxwidth: int;
   maxsize: int;
   maxdepth: int;
+  maxgoalsizefactor : int;
   timeout: float;
   use_library: bool;
   use_paramod: bool;