From 864fda19d046428023851ba540b82c5ca24d06a4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 25 Apr 2018 18:08:39 +0200
Subject: Deprecate most evarutil evdref functions

clear_hyps remain with no alternative
---
 pretyping/coercion.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6dc3687a0..e8b17d694 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -94,7 +94,9 @@ open Program
 
 let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
   let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
-  Evarutil.e_new_evar env evdref ~src c
+  let evd, v = Evarutil.new_evar env !evdref ~src c in
+  evdref := evd;
+  v
 
 let app_opt env evdref f t =
   whd_betaiota !evdref (app_opt f t)
-- 
cgit v1.2.3