aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/equality.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ea74dc37ea..d78ba8c629 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1662,7 +1662,7 @@ let default_subst_tactic_flags () =
else
{ only_leibniz = true; rewrite_dependent_proof = false }
-let regular_subst_tactic = ref false
+let regular_subst_tactic = ref true
let _ =
declare_bool_option