aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--CHANGES2
-rw-r--r--Makefile.common3
2 files changed, 3 insertions, 2 deletions
diff --git a/CHANGES b/CHANGES
index 6335a6b1d7..b02988c8aa 100644
--- a/CHANGES
+++ b/CHANGES
@@ -43,6 +43,8 @@ Vernacular commands
interrupts the interpretation after <n> seconds.
- Option -R now supports binding Coq root read-only.
- New support for local binders in the syntax of Record/Structure fields.
+- Most commands referring to constant (e.g. Print or About) now support
+ referring to the constant by a notation string.
Tools
diff --git a/Makefile.common b/Makefile.common
index 1a6424c950..2db8aabc7d 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -120,8 +120,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
REFMANTEXFILES:=$(addprefix doc/refman/, \
headers.sty Reference-Manual.tex \
RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \
- RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
- ExternalProvers.tex ) \
+ RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \
$(REFMANCOQTEXFILES) \
REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps