aboutsummaryrefslogtreecommitdiff
path: root/kernel/environ.ml
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-21 12:08:44 +0200
committerHugo Herbelin2019-05-21 12:08:44 +0200
commit897088fb8f4769bacca9fc289387096283835cd6 (patch)
tree2934fbca8e3e803e445f84cb65ecf7986c271f50 /kernel/environ.ml
parenta5304d0a613141dd5008410034ae4b104f0fc06a (diff)
parent076932d4bf602560b24c14dc3397e51db5114244 (diff)
Merge PR #10144: Fix #9919: conversion functions are non-linear
Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r--kernel/environ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 97c9f8654a..617519a038 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with
let map_named_val f ctxt =
let open Context.Named.Declaration in
let fold accu d =
- let d' = map_constr f d in
+ let d' = f d in
let accu =
if d == d' then accu
else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu