From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 15:50:17 +0100 Subject: Removing some return type compatibility layers in Termops. --- pretyping/evarsolve.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/evarsolve.ml') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 27436fdd8..3003620d7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -189,8 +189,8 @@ let restrict_evar_key evd evk filter candidates = | None -> evar_filter evi | Some filter -> filter in let candidates = match candidates with - | NoUpdate -> evi.evar_candidates - | UpdateWith c -> Some (List.map EConstr.Unsafe.to_constr c) in + | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | UpdateWith c -> Some c in let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (evk, sigma, _) = restrict_evar sigma evk filter candidates in (Sigma.to_evar_map sigma, evk) -- cgit v1.2.3