summaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:15:04 +0200
commit113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (patch)
treec260a140410c796f113584a2f7e6b9b7f6e00aa5 /dev
parent870075f34dd9fa5792bfbf413afd3b96f17e76a0 (diff)
Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include1
-rw-r--r--dev/db1
-rw-r--r--dev/doc/build-system.txt5
3 files changed, 4 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include
index 398f60d2..0b7a0b67 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,6 +29,7 @@
#install_printer (* qualid *) ppqualid;;
#install_printer (* kernel_name *) ppkn;;
#install_printer (* constant *) ppcon;;
+#install_printer (* cl_index *) ppclindex;;
#install_printer (* constr *) print_pure_constr;;
#install_printer (* patch *) ppripos;;
#install_printer (* values *) ppvalues;;
diff --git a/dev/db b/dev/db
index 6221462a..81878570 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppkn
install_printer Top_printers.ppcon
install_printer Top_printers.ppsp
install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
install_printer Top_printers.ppbigint
install_printer Top_printers.pppattern
diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt
index c9571f7c..9362aeeb 100644
--- a/dev/doc/build-system.txt
+++ b/dev/doc/build-system.txt
@@ -253,9 +253,8 @@ config/Makefile looks like it contains a lot of unused variables,
clean that up (are any maybe used by nightly scripts on
pauillac?). Also, the COQTOP variable from config/Makefile (and used
in contribs) has a very poorly chosen name, because "coqtop" is the
-name of a Coq executable! For example, in the Coq makefile it is
-immediately clobbered by "bin/coqtop$(EXE)"! Rename it to COQROOT or
-COQTREE or COQDIR or ...
+name of a Coq executable! In the coq Makefiles, $(COQTOPEXE) is used
+to refer to that executable.
Promote the granular .glob handling to official way of doing things
for Coq developments, that is implement it in coq_makefile and the