1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* File reduced by coq-bug-finder from 1656 lines to 221 lines to 26 lines to 7 lines. *)
Module Long.
Require Import Corelib.Classes.RelationClasses.
#[export] Hint Extern 0 => apply reflexivity : typeclass_instances.
#[export] Hint Extern 1 => symmetry.
Lemma foo : exists m' : Type, True.
intuition. (* Anomaly: Uncaught exception Not_found. Please report. *)
Abort.
End Long.
Module Short.
Require Import Corelib.Classes.RelationClasses.
#[export] Hint Extern 0 => apply reflexivity : typeclass_instances.
Lemma foo : exists m' : Type, True.
try symmetry. (* Anomaly: Uncaught exception Not_found. Please report. *)
Abort.
End Short.
|
