aboutsummaryrefslogtreecommitdiff
path: root/kernel/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/evd.ml')
-rw-r--r--kernel/evd.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml
index b31f2f6b79..52e1a936eb 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -65,6 +65,4 @@ let is_defined sigma ev =
let info = map sigma ev in
not (info.evar_body = Evar_empty)
-let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
-
let evar_hyps ev = get_globals (context ev.evar_env)