diff options
| author | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-07-26 16:16:08 +0200 |
| commit | dc1db99e019242c07f00837f8316a8d392c40258 (patch) | |
| tree | ff271f3a63d9b4e7e6bf6bde4c590003c549c2c4 /ltac | |
| parent | 139204928e55f92f02d3b3dd1d6746e34fdcdb88 (diff) | |
| parent | 1ca19082cf506c304b3c7945e72c0238f2aa9d1a (diff) | |
Merge branch 'v8.6' into trunk
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0556191be8..e327deda02 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -581,7 +581,7 @@ let general_rewrite_unif_flags () = let core_flags = { rewrite_core_unif_flags with Unification.modulo_conv_on_closed_terms = Some ts; - Unification.use_evars_eagerly_in_conv_on_closed_terms = false; + Unification.use_evars_eagerly_in_conv_on_closed_terms = true; Unification.modulo_delta = ts; Unification.modulo_delta_types = ts; Unification.modulo_betaiota = true } |