diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-17 15:35:49 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-17 15:35:49 +0200 |
commit | 6de02170275e49e5f58a93eb5513d5eb8cb9aa38 (patch) | |
tree | df997be5196651ba2e00910cd681576b36f147d0 /CHANGES | |
parent | 9d8a4a92f75dfc5d831efff4554c28d623d0868f (diff) |
Use the wording suggested by Gaetan.
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -158,7 +158,8 @@ Universes - Cumulative inductive types. see prefixes "Cumulative", "NonCumulative" for inductive definitions and the option "Set Inductive Cumulativity" in the reference manual. -- New syntax `Type@{_}` for anonymous universes. +- New syntax `foo@{_}` to instantiate a polymorphic definition with + anonymous universes (can also be used with `Type`). XML Protocol and internal changes |