diff options
| author | Maxime Dénès | 2019-02-18 23:10:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-18 23:10:28 +0100 |
| commit | 582ba8464962f69f0808ccdd14e7bd64e786875f (patch) | |
| tree | 250229466de145992b823fd36f7bf7cd8560f2a9 /test-suite | |
| parent | 7c62153610f54a96cdded0455af0fff7ff91a53a (diff) | |
| parent | 723f4434d7c715630533031f1bb1522d5d933ce5 (diff) | |
Merge PR #9306: Remove Printing Primitive Projection Compatibility
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_5197.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index b67e93d677..0c236e12ad 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -1,6 +1,6 @@ Set Universe Polymorphism. Set Primitive Projections. -Unset Printing Primitive Projection Compatibility. + Axiom Ω : Type. Record Pack (A : Ω -> Type) (Aᴿ : Ω -> (forall ω : Ω, A ω) -> Type) := mkPack { |