diff options
| author | Matthieu Sozeau | 2019-08-22 17:03:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-08-22 17:03:11 +0200 |
| commit | 41d7105708dbd4a3066a1a92d69ad2547e51ee76 (patch) | |
| tree | 165d8a90504aaa5490925effa51053e79675cebc /plugins | |
| parent | 6bb04f3240e14cc0bbb117879afd0305db31b64c (diff) | |
| parent | 122a5aca4f7b21f65afece2c59e8529183713d71 (diff) | |
Merge PR #9062: Delay the computation of frozen evars in legacy unification.
Reviewed-by: mattam82
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 726752a2bf..1493092f2f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.frozen_evars = Evar.Set.empty; + Unification.allowed_evars = Unification.AllowAll; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; |