The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

The behavior is different in 8.4 (Fixpoint behaves like Definition in 8.4).

I think this deserves a bug report.

Le 02/03/2016 14:58, Ralf Jung a écrit :
> Hi all,
>
> I just noticed that there are some weird differences between Program
> Definition and Program Fixpoint, which force me to use Fixpoint even for
> some non-recursive definition unless I want to spell out some "_"
> explicitly:
>
> ---------- BEGIN --------------
> Require Import Program Omega.
>
> Definition foo (n : nat) {H : n > 5} := n.
>
> Program Fixpoint foo1 x := foo (x + 6).
> Next Obligation. omega. Qed.
>
> (* I would expect this to work. *)
> Fail Program Definition foo1 x := foo (x + 6).
>
>
> (* I can work around it, but it's ugly. *)
> Program Definition foo2 x := foo (x + 6) (H:=_).
> Next Obligation. omega. Qed.
> --------- END ------------
>
> Is this somehow a feature I do not understand, or is it an outright bug
> in "Program"?
>
> In any case, this can be problematic if what you are defining is not a
> function, i.e. does not have any arguments - in that case, you cannot
> use Fixpoint, so you have to be explicit about the "_".
>
> Kind regards,
> Ralf

Attachment: signature.asc
Description: OpenPGP digital signature