From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 2 Apr 2019 13:22:11 +0200 Subject: [api] Remove 8.10 deprecations. Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it. --- engine/evarutil.ml | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) (limited to 'engine/evarutil.ml') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 96beb72a56..be0318fbde 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -26,24 +26,7 @@ let safe_evar_value sigma ev = try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None -(** Combinators *) - -let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - -let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - -let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - -let new_global evd x = +let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in (evd, c) -- cgit v1.2.3