aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/equality.ml')
-rw-r--r--tactics/equality.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8eadd4aee..6c550e916 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -230,8 +230,8 @@ let rewrite_keyed_core_unif_flags = {
(* This is set dynamically *)
restrict_conv_on_strict_subterms = false;
- modulo_betaiota = true;
- (* Different from conv_closed *)
+ modulo_betaiota = false;
+
modulo_eta = true;
}