The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  You should say Next Obligation of doubleE or doubleO. It's debatable
that you need to name them, but
that's the intended behavior. There is a bug in trunk though, it
generates duplicate obligations for each of
doubleE and doubleO, that one should be reported.

Best,
-- Matthieu

2014-12-26 22:41 GMT+01:00 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



-- 
-- Matthieu