diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 4e1636e321..69ee5223c4 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -50,6 +50,18 @@ let new_global evd x = (* Expanding/testing/exposing existential variables *) (****************************************************) +let finalize ?abort_on_undefined_evars sigma f = + let sigma = minimize_universes sigma in + let uvars = ref Univ.LSet.empty in + let v = f (fun c -> + let varsc = EConstr.universes_of_constr sigma c in + let c = EConstr.to_constr ?abort_on_undefined_evars sigma c in + uvars := Univ.LSet.union !uvars varsc; + c) + in + let sigma = restrict_universe_context sigma !uvars in + sigma, v + (* flush_and_check_evars fails if an existential is undefined *) exception Uninstantiated_evar of Evar.t |