diff options
| author | Pierre-Marie Pédrot | 2019-05-03 00:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-11 12:43:22 +0200 |
| commit | 3c6ed7485293c7eb80f9c4d415af0ee0b977f157 (patch) | |
| tree | b7f10c57adf811b57f98fabe5783c6852c19f9d0 /engine/proofview.ml | |
| parent | 15d4547b977e96ed2bc26cea683f5f4f3c9ee137 (diff) | |
Generalize map_named_val to handle whole declarations.
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |