aboutsummaryrefslogtreecommitdiffhomepage
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 506ce4487..2f51ebf2d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -34,6 +34,7 @@ type evar_info = {
evar_hyps : Environ.named_context_val;
evar_body : evar_body}
+val eq_evar_info : evar_info -> evar_info -> bool
val evar_context : evar_info -> named_context
type evar_map