From 9bc1ddceda626730318798e58e7f309e4a334053 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 6 Sep 2017 14:51:12 +0200
Subject: Fix a refine anomaly "Evar defined twice".

Because the argument given to refine may mess with the evarmap, the goal being
refined can be solved by side-effect after the term filler is computed. If this
happens, we simply don't perform the refining operation.
---
 proofs/refine.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/proofs/refine.ml b/proofs/refine.ml
index 4161d71047..e3f6508481 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -102,7 +102,12 @@ let generic_refine ~typecheck f gl =
   in
   (** Proceed to the refinement *)
   let c = EConstr.Unsafe.to_constr c in
-  let sigma = match evkmain with
+  let sigma = match Proofview.Unsafe.advance sigma self with
+  | None ->
+    (** Nothing to do, the goal has been solved by side-effect *)
+    sigma
+  | Some self ->
+    match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
         let id = Evd.evar_ident self sigma in
-- 
cgit v1.2.3