diff options
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 4ae1d034d7..59eea97ce9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -832,9 +832,9 @@ let empty = { extras = Store.empty; } -let from_env e = { empty with universes = UState.from_env e } +let from_env ?binders e = { empty with universes = UState.from_env ?binders e } -let from_ctx ctx = { empty with universes = ctx } +let from_ctx uctx = { empty with universes = uctx } let has_undefined evd = not (EvMap.is_empty evd.undf_evars) @@ -1231,6 +1231,11 @@ let restrict evk filter ?candidates ?src evd = let evd = declare_future_goal evk' evd in (evd, evk') +let update_source evd evk src = + let evar_info = EvMap.find evk evd.undf_evars in + let evar_info' = { evar_info with evar_source = src } in + { evd with undf_evars = EvMap.add evk evar_info' evd.undf_evars } + (**********************************************************) (* Accessing metas *) |