diff options
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 19 |
1 files changed, 1 insertions, 18 deletions
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) |