From 31a35fe712a836c90562edebc01bfcf3d1c6646a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 28 Feb 2018 21:10:38 +0100 Subject: [econstr] Remove some Unsafe.to_constr use. Most of it seems straightforward. --- engine/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine') diff --git a/engine/proofview.ml b/engine/proofview.ml index fdb0a215d..b4afb6415 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -39,7 +39,7 @@ let proofview p = let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in - let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in + let nf0 c = EConstr.(to_constr solution (of_constr c)) in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in -- cgit v1.2.3