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/evarutil.ml | |
| parent | 23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff) | |
| parent | bbde815f8108f4641f5411d03f7a88096cc2221b (diff) | |
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 6cba6f6075..3ef725cbbd 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter candidates = +let restrict_evar evd evk filter ?src candidates = let evd = Sigma.to_evar_map evd in let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in - let evd, evk' = Evd.restrict evk filter ?candidates evd in + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) let new_pure_evar_full evd evi = |