aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 27b04eedb..70ff2e639 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -142,7 +142,8 @@ let unfreeze fs = searchtable := fs
let _ = Summary.declare_summary "search"
{ Summary.freeze_function = freeze;
Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
+ Summary.init_function = init;
+ Summary.survive_section = false }
(**************************************************************************)