diff options
Diffstat (limited to 'test-suite/bugs/closed/3188.v')
| -rw-r--r-- | test-suite/bugs/closed/3188.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v index 09ab4ca583..0117602670 100644 --- a/test-suite/bugs/closed/3188.v +++ b/test-suite/bugs/closed/3188.v @@ -1,8 +1,7 @@ (* File reduced by coq-bug-finder from 1656 lines to 221 lines to 26 lines to 7 lines. *) -Require Import Coq.Classes.RelationClasses. - Module Long. + Require Import Coq.Classes.RelationClasses. Hint Extern 0 => apply reflexivity : typeclass_instances. Hint Extern 1 => symmetry. @@ -12,9 +11,8 @@ Module Long. Abort. End Long. -Require Import Coq.Classes.RelationClasses. - Module Short. + Require Import Coq.Classes.RelationClasses. Hint Extern 0 => apply reflexivity : typeclass_instances. |