diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 09:44:44 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-17 10:38:50 +0100 |
| commit | 20f9a1404f84ddabde2d1cbacc9063d9de87dfa9 (patch) | |
| tree | c4ea3473526002b3c6ff7c6b6caa3413fbacc9c0 /test-suite/bugs/closed/2830.v | |
| parent | 335c960105971b2a86833793d893df4d9d0d1c90 (diff) | |
Revert "Adapting two files from test-suite to now forbidden Require's in modules."
This reverts commit b0fceb96d0aaa2db6e774c629503be459017608e.
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 219838aa3..b72c821df 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 *) -Require Import Program Relations. - Module B. +Require Import Program Relations. + 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 |