diff options
| author | Hugo Herbelin | 2019-05-21 12:08:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-21 12:08:44 +0200 |
| commit | 897088fb8f4769bacca9fc289387096283835cd6 (patch) | |
| tree | 2934fbca8e3e803e445f84cb65ecf7986c271f50 /kernel | |
| parent | a5304d0a613141dd5008410034ae4b104f0fc06a (diff) | |
| parent | 076932d4bf602560b24c14dc3397e51db5114244 (diff) | |
Merge PR #10144: Fix #9919: conversion functions are non-linear
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 2 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 |
2 files changed, 3 insertions, 3 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 diff --git a/kernel/environ.mli b/kernel/environ.mli index 8c6bc105c7..4e6dbbe206 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -134,9 +134,9 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t *) + *** /!\ *** [f t] should be convertible with t, and preserve the name *) val map_named_val : - (constr -> constr) -> named_context_val -> named_context_val + (named_declaration -> named_declaration) -> named_context_val -> named_context_val val push_named : Constr.named_declaration -> env -> env val push_named_context : Constr.named_context -> env -> env |