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.

---
 pretyping/evarconv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6880383a31..400acc25b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1411,11 +1411,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
               refresh_universes ~status:Evd.univ_flexible (Some true)
                 env_evar_unf evd evty
             else evd, evty in
-          let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
-          let evk = fst (destEvar evd ev) in
+          let (evd, evk) = new_pure_evar sign evd evty ~filter in
           evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
           fixed := Evar.Set.add evk !fixed;
-          evd, ev
+          evd, mkEvar (evk, instance)
      in
      let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
      if debug_ho_unification () then
-- 
cgit v1.2.3