@@ -81,6 +81,9 @@ Minor language changes
8181 which may be inferred from the definition of the hole).
8282* Programs with holes can now be compiled.
8383 Attempting to evaluate an expression with a hole results in a run time error.
84+* Dependent pairs now can be specified using a telescope-style syntax, without
85+ requirement of nesting, e.g. it is possible to now write the following:
86+ (a : Type ** n : Nat ** Vect n a)
8487
8588External Dependencies
8689---------------------
@@ -101,9 +104,6 @@ New in 0.10:
101104 Where `CATS` is a whitespace separated list of categoriese. Default is for
102105 all categories to be logged.
103106* New flag `--listlogcats` to list logging categories.`
104−* Dependent pairs now can be specified using a telescope-style syntax, without
105− requirement of nesting, e.g. it is possible to now write the following:
106− (a : Type ** n : Nat ** Vect n a)
107107
108108New in 0.9.20:
109109==============