diff options
author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-17 07:35:57 -0800 |
---|---|---|
committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-02-17 07:35:57 -0800 |
commit | 5968648f9e9db09de462dd8c3530febd66466312 (patch) | |
tree | 32b40e69b44345209042481fef71c26a4525f778 /CHANGES | |
parent | 8dd6d091ffbfa237f7266eeca60187263a9b521f (diff) |
Implement name mangling option
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -74,6 +74,13 @@ Universes - Fix #5726: Notations that start with `Type` now support universe instances with `@{u}`. +Tools + +- Coq can now be run with the option -mangle-names to change the auto-generated + name scheme. This is intended to function as a linter for developments that + want to be robust to changes in auto-generated names. This feature is experimental, + and may change or dissapear without warning. + Checker - The checker now accepts filenames in addition to logical paths. |