From 1888527bb43d6a8c801565af3e6376c91769fbc1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 9 Sep 2016 11:51:51 +0200 Subject: Removing the now useless field env_named_val from named_context_val. This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead. --- kernel/environ.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'kernel/environ.ml') 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. -- cgit v1.2.3