diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.md | 8 | ||||
| -rw-r--r-- | dev/doc/profiling.txt | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index bb8189efc7..f3fc126f92 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,14 @@ ### ML API +Names + +- In `Libnames`, the type `reference` and its two constructors `Qualid` and + `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, + `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be + replaced by a test using `qualid_is_ident`. Extracting the ident part of a + qualid can be done using `qualid_basename`. + Misctypes - Syntax for universe sorts and kinds has been moved from `Misctypes` diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 9d2ebf0d4c..b5dd8445db 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.1+fp +opam switch 4.02.3+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v |