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 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3