diff options
| author | Hugo Herbelin | 2015-01-04 13:02:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-04 13:05:50 +0100 |
| commit | b0fceb96d0aaa2db6e774c629503be459017608e (patch) | |
| tree | f3393c4ea8b04648d63e1d5d42aae3d7da38181f | |
| 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?).
| -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 8874ce9e50..8149065e72 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 0117602670..09ab4ca583 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. |