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 /engine | |
| 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 'engine')
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 0f10a380d3..15b4c31851 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 1fd8b5d50e..5c5a02d3fa 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 |