diff options
| author | Maxime Dénès | 2020-09-02 18:10:37 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-09-02 21:50:13 +0200 |
| commit | cd37a10f9cf5746edf16611d7f833e0e8cf2c5f8 (patch) | |
| tree | 98820e613bcde15378375cb06f9134e29f122d16 /plugins/ltac | |
| parent | fea073c74f98f3fe6728363c0f8142520ac1e50c (diff) | |
Abstract type for allowed evars
Diffstat (limited to 'plugins/ltac')
| -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 a8a3a21f4a..a1dbf9a439 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.allowed_evars = Evarsolve.AllowAll; + Unification.allowed_evars = Evarsolve.AllowedEvars.all; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; |