Ssreflect Users Discussion List

[Marcus Ramos <>]

Hi,

When I try to run the example of page 22 of the tutorial ("An introduction to small scale reflection in Coq") I get an error message and can´t understand why. See below:

Section Page_22.

Variables P Q: bool->Prop.

Hypothesis P2Q: forall a b, P(a || b)-> Q a.

Goal forall a, P (a || a) -> True.

move => a HPa.

(* error occurs in the next line *)

move: {HPa}(P2Q _ _ HPa) => HQa.

The error message (Proof General/Windows) is:

Toplevel input, characters 12-19:

Error: Illegal application (Non-functional construction): 

The _expression_ "P2Q ?9" of type "Q ?7"

cannot be applied to the term

 "?11" : "?10"

Any help appreciated. By the way, the next two examples work fine.

Thanks,

Marcus.