diff options
Diffstat (limited to 'test-suite/success/dependentind.v')
| -rw-r--r-- | test-suite/success/dependentind.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f5bb884d..55ae54ca 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -42,7 +42,7 @@ Inductive ctx : Type := Bind Scope context_scope with ctx. Delimit Scope context_scope with ctx. -Arguments Scope snoc [context_scope]. +Arguments snoc _%context_scope. Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. |