diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:12:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-02 15:25:14 +0200 |
| commit | b6b98a67c65d7aeeeeca12d1ccb9d55b654c554d (patch) | |
| tree | 2a90fbdf676aea46265fc5dd45ed220a47d9ff82 /dev | |
| parent | 4648732544f43ad87266f33967995b29d2b8338b (diff) | |
A slight phase of documentation and uniformization of names of
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 53497ff0e..4a0130bef 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,10 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Notation_ops ** + +Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. + ** Logging and Pretty Printing: ** * Printing functions have been removed from `Pp.mli`, which is now a |