diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-04 13:02:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-04 13:05:50 +0100 |
| commit | b0fceb96d0aaa2db6e774c629503be459017608e (patch) | |
| tree | f3393c4ea8b04648d63e1d5d42aae3d7da38181f /test-suite | |
| parent | 3cd718c8f7b48bae776b62ffafa1aa7e18218ed4 (diff) | |
Adapting two files from test-suite to now forbidden Require's in modules.
Status of 335 and 3363 which are explicitly testing Require in modules
still to be addressed (to remove from test suite?).
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/2830.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3188.v | 6 |
2 files changed, 6 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v index 8874ce9e5..8149065e7 100644 --- a/test-suite/bugs/closed/2830.v +++ b/test-suite/bugs/closed/2830.v @@ -39,10 +39,10 @@ End A. (* 2- This was submitted by Andrew Appel *) -Module B. - Require Import Program Relations. +Module B. + Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) := { af_unage : forall x x' y', level x' = level y' -> age1 x = Some x' -> exists y, age1 y = Some y' ; af_level1 : forall x, age1 x = None <-> level x = 0 diff --git a/test-suite/bugs/closed/3188.v b/test-suite/bugs/closed/3188.v index 011760267..09ab4ca58 100644 --- a/test-suite/bugs/closed/3188.v +++ b/test-suite/bugs/closed/3188.v @@ -1,7 +1,8 @@ (* 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. @@ -11,8 +12,9 @@ Module Long. Abort. End Long. +Require Import Coq.Classes.RelationClasses. + Module Short. - Require Import Coq.Classes.RelationClasses. Hint Extern 0 => apply reflexivity : typeclass_instances. |