aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-05-03 00:41:55 +0200
committerPierre-Marie Pédrot2019-05-11 12:43:22 +0200
commit3c6ed7485293c7eb80f9c4d415af0ee0b977f157 (patch)
treeb7f10c57adf811b57f98fabe5783c6852c19f9d0 /engine/evd.ml
parent15d4547b977e96ed2bc26cea683f5f4f3c9ee137 (diff)
Generalize map_named_val to handle whole declarations.
Diffstat (limited to 'engine/evd.ml')
-rw-r--r--engine/evd.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index b89222cf8e..96c2719f8f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -222,7 +222,7 @@ let map_evar_body f = function
let map_evar_info f evi =
{evi with
evar_body = map_evar_body f evi.evar_body;
- evar_hyps = map_named_val f evi.evar_hyps;
+ evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps;
evar_concl = f evi.evar_concl;
evar_candidates = Option.map (List.map f) evi.evar_candidates }