From c0a71f9ff6289d99bbbcd13ef65c68f74ac9e191 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 12 Feb 2020 10:27:13 +0100 Subject: Remove special case for implicit inductive parameters Co-authored-by: Jasper Hugunin Co-authored-by: Gaëtan Gilbert --- test-suite/bugs/closed/bug_11585.v | 3 +++ test-suite/bugs/closed/bug_5233.v | 3 +++ 2 files changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/bug_11585.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/bug_11585.v b/test-suite/bugs/closed/bug_11585.v new file mode 100644 index 0000000000..6294668323 --- /dev/null +++ b/test-suite/bugs/closed/bug_11585.v @@ -0,0 +1,3 @@ +Fail Inductive type {type : Type} : Type := T : type. + +Inductive type {type : Type} : Type := T . diff --git a/test-suite/bugs/closed/bug_5233.v b/test-suite/bugs/closed/bug_5233.v index 06286c740d..63e33b63f7 100644 --- a/test-suite/bugs/closed/bug_5233.v +++ b/test-suite/bugs/closed/bug_5233.v @@ -1,2 +1,5 @@ (* Implicit arguments on type were missing for recursive records *) Inductive foo {A : Type} : Type := { Foo : foo }. + +(* Implicit arguments can be overidden *) +Inductive bar {A : Type} : Type := { Bar : @bar (A*A) }. -- cgit v1.2.3