aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-02-17 07:35:57 -0800
committerGravatar Jasper Hugunin <jasperh@cs.washington.edu>2018-02-17 07:35:57 -0800
commit5968648f9e9db09de462dd8c3530febd66466312 (patch)
tree32b40e69b44345209042481fef71c26a4525f778 /CHANGES
parent8dd6d091ffbfa237f7266eeca60187263a9b521f (diff)
Implement name mangling option
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES7
1 files changed, 7 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 8d344d4f0..449d346b0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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.