diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.md | 4 | ||||
| -rw-r--r-- | dev/doc/univpoly.txt | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 707adce308..c69be4f4de 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -46,9 +46,9 @@ We changed the type of the following functions: - `Global.body_of_constant`: same as above. -We renamed the following datatypes: +We have changed the representation of the following types: -- `Pp.std_ppcmds` -> `Pp.t` +- `Lib.object_prefix` is now a record instead of a nested tuple. Some tactics and related functions now support static configurability, e.g.: diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 6a69c57934..ca3d520c70 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -12,7 +12,7 @@ type pinductive = inductive puniverses type pconstructor = constructor puniverses type constr = ... - | Const of puniversess + | Const of puniverses | Ind of pinductive | Constr of pconstructor | Proj of constant * constr |