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 /pretyping/evarconv.ml | |
| parent | fea073c74f98f3fe6728363c0f8142520ac1e50c (diff) | |
Abstract type for allowed evars
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3dc00d195e..61453ff214 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full let default_flags_of ?(subterm_ts=TransparentState.empty) ts = { modulo_betaiota = true; open_ts = ts; closed_ts = ts; subterm_ts; - allowed_evars = AllowAll; with_cs = true; + allowed_evars = AllowedEvars.all; with_cs = true; allow_K_at_toplevel = true } let default_flags env = @@ -1209,7 +1209,7 @@ let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat = | Success sigma -> true, sigma | UnifFailure _ -> false, sigma -let default_occurrences_selection ?(allowed_evars=AllowAll) ts n = +let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n = (default_occurrence_test ~allowed_evars ts, List.init n (fun _ -> default_occurrence_selection)) |