Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Uncaught exception upon destructing a disjunction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Uncaught exception upon destructing a disjunction


Chronological Thread 
  • From: Gabriel Scherer <gabriel.scherer AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Uncaught exception upon destructing a disjunction
  • Date: Mon, 11 Dec 2017 09:18:28 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f169.google.com
  • Ironport-phdr: 9a23:uu2gnxbqckQ3zxjFsqOB42L/LSx+4OfEezUN459isYplN5qZpsW9bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76xXcoFx7+LQt4IPjuUs6X1pzvlrP6x5qGSAJRzBG5fLk6eB6xtEDastQcqYpkMKc4jBXT9ChmYeNTkExhL0iSkhK03cyw8YRu6WwEtPsr7c9NVePhdKQ1V7FCJDsjOmExosbssE+QHkO0+nIAXzBOwVJzCA/f4US/B8+pvw==
Yes, this is a bug. I can reproduce it on 8.6, but I don't know about 8.7.

Note that the code you wrote is incorrect as the "as" part does not have the shape of a disjunction [ ... | ... ] as it should. You should write

  intros A H; destruct H as [ H | H ].

or even

  intros A [ H | H ].

On Sun, Dec 10, 2017 at 6:58 AM, Bruno Le Floch <blflatex AT gmail.com> wrote:
Hi all,

Is this a bug?  Given a file containing the four non-blank lines
following this paragraph, running "coqc <filename>.v" produces the
two-line error below.  Coq version 8.5pl2 (August 2016) compiled with
OCaml 4.01.0.


Theorem test : forall A : Prop, A \/ A -> A.
Proof.
  intros A.
  intros H ; destruct H as H.


File "./Experiment3.v", line 4, characters 13-28:
Anomaly: Uncaught exception Not_found. Please report.


Best regards,
Bruno


Archive powered by MHonArc 2.6.18.

Top of Page