diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 19:56:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-15 19:56:14 +0200 |
| commit | a8c6eeeaa321a84063e8492aca25942a07c00ddb (patch) | |
| tree | 9dc837006893ad9e92db939298ce336246b07a48 /test-suite/bugs/opened | |
| parent | 425c158e83e86471f5463e75cce2b6a6daa4e7c6 (diff) | |
Fix test-suite for opened bug #4813.
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/4813.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v index 7c65accfe..b75170179 100644 --- a/test-suite/bugs/opened/4813.v +++ b/test-suite/bugs/opened/4813.v @@ -2,4 +2,4 @@ Record T := BT { t : Set }. Record U (x : T) := BU { u : t x -> Prop }. -Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. +Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. |