diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 17 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 |
2 files changed, 8 insertions, 11 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 09e49f3253..4d5715a391 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -29,27 +29,24 @@ module AllowedEvars = struct type t = | AllowAll - | AllowFun of (Evar.t -> bool) + | AllowFun of (Evar.t -> bool) * Evar.Set.t let mem allowed evk = match allowed with | AllowAll -> true - | AllowFun f -> f evk + | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except) - let remove evk allowed = - let allowed = match allowed with - | AllowAll -> fun evk' -> not (Evar.equal evk evk') - | AllowFun f -> fun evk' -> not (Evar.equal evk evk') && f evk' - in - AllowFun allowed + let remove evk = function + | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk) + | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except) let all = AllowAll let except evars = - AllowFun (fun evk -> not (Evar.Set.mem evk evars)) + AllowFun ((fun _ -> true), evars) let from_pred f = - AllowFun f + AllowFun (f, Evar.Set.empty) end diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 746a237b24..207a03d80f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -417,7 +417,7 @@ let default_no_delta_unify_flags ts = let allow_new_evars sigma = let undefined = Evd.undefined_map sigma in - AllowedEvars.except @@ Evar.Map.domain 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 *) |