aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/evd.mli')
-rw-r--r--engine/evd.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.mli b/engine/evd.mli
index 7876e9a48f..8843adc853 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -125,8 +125,8 @@ val evar_filtered_hyps : evar_info -> named_context_val
val evar_body : evar_info -> evar_body
val evar_candidates : evar_info -> constr list option
val evar_filter : evar_info -> Filter.t
-val evar_env : evar_info -> env
-val evar_filtered_env : evar_info -> env
+val evar_env : env -> evar_info -> env
+val evar_filtered_env : env -> evar_info -> env
val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info