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: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr, Bruno Le Floch <blflatex AT gmail.com>
  • Subject: Re: [Coq-Club] Uncaught exception upon destructing a disjunction
  • Date: Mon, 11 Dec 2017 09:18:03 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:H8md1hxnhxJp2C/XCy+O+j09IxM/srCxBDY+r6Qd0uIQIJqq85mqBkHD//Il1AaPBtqLra8cw8Pt8IneGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2NBXupSi56idXERHiPyJ0IP70E8jclYD//fqv/ZqbRwgAqj66arM6eB+yowHYqsQGqYRnI6c1jBDOpy0bVf5RwDZSLFad1zTh4Mj4qJx+9St4vuogstVfSuP9ZatuHu8QNygvL21gvJ6jjhLEVwbavnY=
Hi Bruno,

> 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.

This is definitely a bug! Coq 8.5 is pretty ancient (the current
version is 8.7), but in fact the issue reproduces with Coq 8.7.

Can you report this at <https://github.com/coq/coq/issues/>?

Kind regards,
Ralf

Archive powered by MHonArc 2.6.18.

Top of Page