set_solve_evars doesn't use an evar_map ref

1 files changed, 7 insertions, 6 deletions

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 ->