The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I tried this in Coq 8.4pl4:

Require Import Program.

Inductive Even : nat -> Prop := 

| evenO : Even O

| evenS : forall n, Odd n -> Even (S n)

with Odd : nat -> Prop :=

| oddS : forall n, Even n -> Odd (S n).

Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n)

  := _

with doubleO {n} (o : Odd n) : Odd (S (2 * n))

     := _.

Next Obligation. (* Error: More than one program with unsolved obligations *)

bug got "Error: More than one program with unsolved obligations".  Is there a way to fix this?  Is this a bug that should be reported?

Thanks,

Jason