aboutsummaryrefslogtreecommitdiff
path: root/kernel/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/evd.ml')
-rw-r--r--kernel/evd.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 6853fc9c46..b482f94538 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -66,6 +66,7 @@ let is_defined sigma ev =
not (info.evar_body = Evar_empty)
let evar_hyps ev = var_context ev.evar_env
+let evar_body ev = ev.evar_body
let id_of_existential ev =
id_of_string ("?" ^ string_of_int ev)