aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 231a17f852..0e66c43c3b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -850,7 +850,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
Auto.default_auto
]);
Equality.general_rewrite_bindings_in true
- all_occurrences
+ all_occurrences false
(List.hd !avoid)
((mkVar (List.hd (List.tl !avoid))),
Rawterm.NoBindings