From 3c6ed7485293c7eb80f9c4d415af0ee0b977f157 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 3 May 2019 00:41:55 +0200
Subject: Generalize map_named_val to handle whole declarations.

---
 engine/evd.ml       | 2 +-
 engine/proofview.ml | 2 +-
 kernel/environ.ml   | 2 +-
 kernel/environ.mli  | 4 ++--
 4 files changed, 5 insertions(+), 5 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 }
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f278c83912..6992d15fcb 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -46,7 +46,7 @@ let compact el ({ solution } as pv) =
   let apply_subst_einfo _ ei =
     Evd.({ ei with
        evar_concl =  nf ei.evar_concl;
-       evar_hyps = Environ.map_named_val nf0 ei.evar_hyps;
+       evar_hyps = Environ.map_named_val (fun d -> map_constr nf0 d) ei.evar_hyps;
        evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
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
-- 
cgit v1.2.3