diff options
| author | Matthieu Sozeau | 2016-02-02 15:28:48 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-02-23 18:23:18 +0100 |
| commit | 55ce331822a673d710451c628ec5a731ab36da1f (patch) | |
| tree | 2f2bbe46afbc34ceddc1efbe0143bad37fcb07be | |
| parent | e54d014ce10dea4a74b66e5091d25e4b26bd71fa (diff) | |
Fix bug #4544: Backtrack on using full betaiota reduction during keyed unification.
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ef1ec13bae..80f6038cb7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -228,8 +228,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; } |