aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 86ec47d3e..53956f99b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -111,10 +111,11 @@ val evar_concl : evar_info -> constr
val evar_context : evar_info -> named_context
val evar_filtered_context : evar_info -> named_context
val evar_hyps : evar_info -> named_context_val
+val evar_filtered_hyps : evar_info -> named_context_val
val evar_body : evar_info -> evar_body
val evar_filter : evar_info -> bool list
-val evar_unfiltered_env : evar_info -> env
val evar_env : evar_info -> env
+val evar_filtered_env : evar_info -> env
(*** Unification state ***)
type evar_map