diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/dependentind.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 8b8ce00987..be7b77ef00 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -35,7 +35,7 @@ Inductive ctx : Type := | empty : ctx | snoc : ctx -> type -> ctx. -Notation " Γ , τ " := (snoc Γ τ) (at level 20, t at next level). +Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity). Fixpoint conc (Γ Δ : ctx) : ctx := match Δ with @@ -43,7 +43,7 @@ Fixpoint conc (Γ Δ : ctx) : ctx := | snoc Δ' x => snoc (conc Γ Δ') x end. -Notation " Γ ; Δ " := (conc Γ Δ) (at level 20). +Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity). Inductive term : ctx -> type -> Type := | ax : forall Γ τ, term (Γ, τ) τ |