diff options
| author | Pierre-Marie Pédrot | 2020-09-03 12:46:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-03 12:46:59 +0200 |
| commit | b3bf44f21581fc72f4087e42a192f15242a545e9 (patch) | |
| tree | a397c05ba649bccc3859a5e16f1140b4ec9e9d16 /pretyping/unification.ml | |
| parent | 5ea743ed08f96013438b6ff54b81745e4191d3c6 (diff) | |
| parent | 6f3d15a9edc2e04e973c47ee20093a1f79a990cf (diff) | |
Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay them
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a26c981cb9..207a03d80f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -252,10 +252,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) - type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) @@ -289,7 +285,7 @@ type core_unify_flags = { (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *) (* when ?B is a Meta. *) - allowed_evars : allowed_evars; + allowed_evars : AllowedEvars.t; (* Evars that are allowed to be instantiated *) (* Useful e.g. for autorewrite *) @@ -341,7 +337,7 @@ let default_core_unify_flags () = check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -421,7 +417,7 @@ let default_no_delta_unify_flags ts = let allow_new_evars sigma = let undefined = Evd.undefined_map sigma in - AllowFun (fun evk -> not (Evar.Map.mem evk undefined)) + AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined)) (* Default flags for looking for subterms in elimination tactics *) (* Not used in practice at the current date, to the exception of *) @@ -604,9 +600,8 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, Stack.empty)) -let is_evar_allowed flags evk = match flags.allowed_evars with -| AllowAll -> true -| AllowFun f -> f evk +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> is_evar_allowed flags evk |