From 834c64015b608b8152e160d37e6f07a3106ff26b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 20:02:42 +0200
Subject: Remove Evarutil.new_evar_instance from the API.

---
 proofs/clenv.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'proofs/clenv.ml')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4d148756b4..9bd7ccda5d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -781,7 +781,8 @@ let make_evar_clause env sigma ?len t =
         Some (ctx, args, subst), ctx, args, subst
       | Some (ctx, args, subst) -> inst, ctx, args, subst
       in
-      let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in
+      let (sigma, ev) = new_pure_evar ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) in
+      let ev = mkEvar (ev, args) in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
-- 
cgit v1.2.3