summaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 4813d3b9..dbaf803b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -127,6 +127,7 @@ 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