coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] assert failure (file "tactics/decl_proof_instr.ml", line 918, characters 3-9)

From: Vag Vagoff <vag.vagoff AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] assert failure (file "tactics/decl_proof_instr.ml", line 918, characters 3-9)
Date: Mon, 18 Apr 2011 18:02:49 +0300
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:user-agent:mime-version:to:subject :content-type:content-transfer-encoding; b=G8Dyj6trd6mXBJLoeIP1PImDA7YYVjd74dOyif5iOOGoFRWyhH9+q4TVB5DuWSCbJ9 TIfzYCnYxOiuwqxTAMcdw7aJ/nVDopUI6REH+/N+BYy19gehwPAscaVICm2T9C45eTGZ qLULJv8PwpR5H2NNL7ZpVvFf6DA0QVJ6G30RQ=

Anomaly: assert failure
(file "tactics/decl_proof_instr.ml", line 918, characters 3-9).
Please report.

---------------------------------------------------------------
Section Context.
Variable p q : Prop.

Theorem nandn: ~ p /\ ~ q <-> ~ (p \/ q).
proof.
    focus on ( ~ p /\ ~ q -> ~ (p \/ q) ).
        assume (~ p /\ ~ q) and H:(p \/ q).
        per cases of H:(p \/ q).
        (* I know there must be "per cases of (p \/ q) by H.", but as it asks
to report... *)
---------------------------------------------------------------
Vag.

(Coq version 8.3)

[Coq-Club] assert failure (file "tactics/decl_proof_instr.ml", line 918, characters 3-9), Vag Vagoff