The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 15 sept. 09 à 11:12, Adam Koprowski a écrit :

   Dear all,

Dear Adam,

  Apologies for a silly question but I spent quite some time trying to figure it out on my own with no luck...
  How can I provide a measure annotation for a Fixpoint built using Program, if the measure depends on more than one argument? The following snippet worked just fine in the trunk (one day) but now I did not manage to achieve a similar effect with 8.2pl1 (not for the lack of trying):

Program Fixpoint test (e : exp | correct e) (s : string) { measure (build_pcx (e, s)) (pcx_lt) } : ...

You have to manually decurryfy so that test takes a pair. Program does it for you in the trunk.

The measure annotation is somewhat different too.

-- Matthieu