aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-31 16:58:29 +0200
committerMaxime Dénès2017-05-31 16:58:29 +0200
commiteed90d1bd867dce59f6bf1b2bf769fff188f128b (patch)
treecfbf3bb666b23d0ddce9ea3c370c54eb4a87a150 /engine/evd.mli
parent23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff)
parentbbde815f8108f4641f5411d03f7a88096cc2221b (diff)
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 0053324706..86755c360b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
(** {6 Misc} *)
val restrict : evar -> Filter.t -> ?candidates:constr list ->
- evar_map -> evar_map * evar
+ ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
(** Restrict an undefined evar into a new evar by filtering context and
possibly limiting the instances to a set of candidates *)