summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3732.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3732.v')
-rw-r--r--test-suite/bugs/closed/3732.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
index 09f1149c..13d62b8f 100644
--- a/test-suite/bugs/closed/3732.v
+++ b/test-suite/bugs/closed/3732.v
@@ -16,7 +16,7 @@ Section machine.
| Inj : forall G, Prop -> propX G
| ExistsX : forall G A, propX (A :: G) -> propX G.
- Implicit Arguments Inj [G].
+ Arguments Inj [G].
Definition PropX := propX nil.
Fixpoint last (G : list Type) : Type.