diff options
| author | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
| commit | eed90d1bd867dce59f6bf1b2bf769fff188f128b (patch) | |
| tree | cfbf3bb666b23d0ddce9ea3c370c54eb4a87a150 /engine/evd.ml | |
| parent | 23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff) | |
| parent | bbde815f8108f4641f5411d03f7a88096cc2221b (diff) | |
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b677705bc9..48fceae9ec 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -653,12 +653,13 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } -let restrict evk filter ?candidates evd = +let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in let evar_info' = { evar_info with evar_filter = filter; evar_candidates = candidates; + evar_source = (match src with None -> evar_info.evar_source | Some src -> src); evar_extra = Store.empty } in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods |