aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r--kernel/environ.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f4a3312ef..96e35610c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -100,7 +100,6 @@ let fold_rel_context f env ~init =
(* Named context *)
let named_context_of_val c = c.env_named_ctx
-let named_vals_of_val c = c.env_named_val
(* [map_named_val f ctxt] apply [f] to the body and the type of
each declarations.