diff options
| author | Hugo Herbelin | 2020-11-14 16:14:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-24 15:29:16 +0100 |
| commit | 47910007a9eff37c9f364a269b46874165711abf (patch) | |
| tree | 6d9a6cc4b77840ea045e6c5d68d7c5c1cd152484 /engine/evd.ml | |
| parent | 90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (diff) | |
Add a new evar source to refer to evars which are types of evars.
To tie the knot (since the evar depends on the evar type and the
source of the evar type of the evar), we use an "update_source"
function.
An alternative could be to provide a function to build both an evar
with its evar type directly in evd.ml...
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 498a9d9825..59eea97ce9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -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 *) |