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

1 files changed, 30 insertions, 0 deletions

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.