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/bugs/closed/2830.v | |
| 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/bugs/closed/2830.v')
| -rw-r--r-- | test-suite/bugs/closed/2830.v | 4 |
1 files changed, 2 insertions, 2 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 |