From 8894e9eb35e5529966fea699014fef83e4b270bd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 26 Apr 2018 14:29:34 +0200
Subject: set_solve_evars doesn't use an evar_map ref

---
 pretyping/evarconv.ml  | 13 +++++++------
 pretyping/evarconv.mli |  2 +-
 pretyping/typing.ml    |  7 ++++++-
 3 files changed, 14 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2144639d5..49c429458 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1159,17 +1159,18 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
 
   let subst = make_subst (ctxt,Array.to_list args,argoccs) in
 
-  let evdref = ref evd in
-  let rhs = set_holes evdref rhs subst in
-  let evd = !evdref in
+  let evd, rhs =
+    let evdref = ref evd in
+    let rhs = set_holes evdref rhs subst in
+    !evdref, rhs
+  in
 
   (* We instantiate the evars of which the value is forced by typing *)
   let evd,rhs =
-    let evdref = ref evd in
-    try let c = !solve_evars env_evar evdref rhs in !evdref,c
+    try !solve_evars env_evar evd rhs
     with e when Pretype_errors.precatchable_exception e ->
       (* Could not revert all subterms *)
-      raise (TypingFailed !evdref) in
+      raise (TypingFailed evd) in
 
   let rec abstract_free_holes evd = function
   | (id,idty,c,_,evsref,_,_)::l ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index bea3eeb2e..cdf5dd0e5 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -69,7 +69,7 @@ val second_order_matching : transparent_state -> env -> evar_map ->
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
-val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit
+val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
 
 type unify_fun = transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index da72d7a75..281e33e9b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -443,4 +443,9 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> e_solve_evars env evdref c)
+let solve_evars env sigma c =
+  let evdref = ref sigma in
+  let c = e_solve_evars env evdref c in
+  !evdref, c
+
+let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c)
-- 
cgit v1.2.3