aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-04-17 11:42:40 +0200
committerEmilio Jesus Gallego Arias2019-04-17 11:42:40 +0200
commit11dd3aeedd5662ea67c89bacb02cce5b562a9532 (patch)
tree7cf700204ad4f7163f9a2fd591101887567a70ba
parent14a51bd079fb3ba5d2eece1dced219ce66702694 (diff)
parent1797f8610106d7a4a0b20523a2860e73a9f985cb (diff)
Merge PR #9966: Add changes for -set
-rw-r--r--CHANGES.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md
index ce8a787cd1..d441200890 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -227,6 +227,8 @@ Tools
`coqc`/`make` as well as printing to stdout, on both python2 and
python3.
+- Coq options can be set on the command line, eg `-set "Universe Polymorphism=true"`
+
Standard Library
- Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about