From 5e8824960f68f529869ac299b030282cc916ba2c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 28 Jan 2013 18:02:02 +0000
Subject: Fixing one part of #2830 (anomaly "defined twice" due to nested calls
 to the function solve_candidates introduced in 8.4).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16163 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b6e8f9d138..c2ba6d9575 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1506,7 +1506,10 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
           (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
       | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
-      | [c,evd] -> Evd.define evk c evd
+      | [c,evd] ->
+          (* solve_candidates might have been called recursively in the mean *)
+          (* time and the evar been solved by the filtering process *)
+          if Evd.is_undefined evd evk then Evd.define evk c evd else evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
           restrict_evar evd evk None (Some candidates)
-- 
cgit v1.2.3