Coqを落すコード

coq

Coqを使っていたら、coqcを落すコードに出会ってしまいました。

コード

Require Import Sets.Ensembles.

Variable (P: Prop).
Variable (A: Type).

Hypothesis the_hypo :
  forall x, exists xs, In A xs x -> P.

Theorem some_theorem :
  P -> P.
Proof.
intros.
apply the_hypo in H.
(* Anomaly: uncaught exception Not_found. Please report. *)

症状

これをコンパイルしようとすると、コンパイラが落ちます。

$ coqc bug.v
File "./bug.v", line 13, characters 0-19:
Anomaly: uncaught exception Not_found. Please report.

動作環境

ちなみにCoqはSnowLeopardで動いてます。

$ coqc -v
The Coq Proof Assistant, version 8.2pl1 (October 2009)
compiled on Oct 31 2009 09:59:41 with OCaml 3.11.1

わかってること

apply the_hypo in H.はダメだけど、apply the_hypo in |- *.は平気です。