diff options
Diffstat (limited to 'test-suite/success/Inversion.v')
| -rw-r--r-- | test-suite/success/Inversion.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 1dbeaf3e1f..8297f54641 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Arguments NL [I]. +Arguments NL {I}. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := |