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

2 files changed, 34 insertions, 1 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b6e8f9d13..c2ba6d957 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)
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
new file mode 100644
index 000000000..2daff6123
--- /dev/null
+++ b/test-suite/bugs/closed/2830.v
@@ -0,0 +1,30 @@
+Set Implicit Arguments.
+
+Inductive Bit := O | I.
+
+Inductive BitString: nat -> Set :=
+| bit: Bit -> BitString 0
+| bitStr: forall n: nat, Bit -> BitString n -> BitString (S n).
+
+Definition BitOr (a b: Bit) :=
+  match a, b with
+  | O, O => O
+  | _, _ => I
+  end.
+
+(* Should fail with an error; used to failed in 8.4 and trunk with
+   anomaly Evd.define: cannot define an evar twice *)
+
+Fail Fixpoint StringOr (n m: nat) (a: BitString n) (b: BitString m) :=
+  match a with
+  | bit a' =>
+      match b with
+      | bit b' => bit (BitOr a' b')
+      | bitStr b' bT => bitStr b' (StringOr (bit a') bT)
+      end
+  | bitStr a' aT =>
+      match b with
+      | bit b' => bitStr a' (StringOr aT (bit b'))
+      | bitStr b' bT => bitStr (BitOr a' b') (StringOr aT bT)
+      end
+  end.