13 files changed, 16 insertions, 275 deletions
diff --git a/dev/README b/dev/README
index 814f60957..b446c3e97 100644
--- a/dev/README
+++ b/dev/README
@@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
 Other development tools (directory tools)
 -----------------------
 
-Makefile.dir: makefile dedicated to intensive work in a given directory
-Makefile.subdir: makefile dedicated to intensive work in a given subdirectory
-Makefile.devel: utilities to automatically launch coq in various states
-Makefile.common: used by other Makefiles
 objects.el: various development utilities at emacs level
 anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
   location of Anomaly backtraces and jump to them conveniently from
diff --git a/dev/TODO b/dev/TODO
deleted file mode 100644
index e62ee6e53..000000000
--- a/dev/TODO
+++ /dev/null
@@ -1,22 +0,0 @@
-
- o options de la ligne de commande
-     - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
-
- o arguments implicites
-     - les calculer une fois pour toutes à la déclaration (dans Declare)
-       et stocker cette information dans le in_variable, in_constant, etc.
-
- o Environnements compilés (type Environ.compiled_env)
-     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
-
- o Efficacité
-     - utiliser DOPL plutôt que DOPN (sauf pour Case)
-     - batch mode => pas de undo, ni de reset
-     - conversion : déplier la constante la plus récente
-     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
-       lookup_mind_specif
-
- o Toplevel
-     - parsing de la ligne de commande : utiliser Arg ???
-
-
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index b43ada907..cbe2a5186 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -4,19 +4,13 @@
 set -e
 
 # Configuration setup
-eval `opam config env`
-make distclean
 OUTDIR=$PWD/_install
 DMGDIR=$PWD/_dmg
-./configure -debug -prefix $OUTDIR -native-compiler no
 VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
 
 # Create a .app file with CoqIDE
-~/.local/bin/jhbuild run make -j -l2 $APP
-
-# Build Coq and run test-suite
-make && make check
+make -j $NJOBS -l2 $APP
 
 # Add Coq to the .app file
 make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
@@ -29,7 +23,9 @@ mkdir -p $DMGDIR
 ln -sf /Applications $DMGDIR/Applications
 cp -r $APP $DMGDIR
 
+mkdir -p _build
+
 # Temporary countermeasure to hdiutil error 5341
-head -c9703424 /dev/urandom > $DMGDIR/.padding
+# head -c9703424 /dev/urandom > $DMGDIR/.padding
 
-hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
+hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index e8018158b..b610f7000 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -7,4 +7,4 @@ coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
 
 git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
 
-( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) )
+( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make test-suite )
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
deleted file mode 100644
index f4b4a425e..000000000
--- a/dev/db_printers.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-open Pp
-open Names
-
-let pp s = pp (hov 0 s)
-
-let prid id = Format.print_string (Id.to_string id)
-let prsp sp = Format.print_string (DirPath.to_string sp)
-
-
diff --git a/dev/doc/api.txt b/dev/doc/api.txt
deleted file mode 100644
index 5827257b5..000000000
--- a/dev/doc/api.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-Recommendations in using the API:
-
-The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
-
-- On type constr, the canonical equality on CIC (up to
-  alpha-conversion and cast removal) is Constr.equal
-- The type constr is abstract, use mkRel, mkSort, etc. to build
-  elements in constr; use "kind_of_term" to analyze the head of a
-  constr; use destRel, destSort, etc. when the head constructor is
-  known
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index a48c491d3..0f1a28028 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -188,6 +188,9 @@ In Coqlib / reference location:
 - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
   was very specific. Use tclPROGRESS instead.
 
+- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows
+  to iterate a non-unit tactic on all goals and access their returned values.
+
 - The unsafe flag of the Refine.refine function and its variants has been
   renamed and dualized into typecheck and has been made mandatory.
 
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v
index a81f170c6..a81f170c6 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion.v
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
deleted file mode 100644
index ffdb1bdca..000000000
--- a/dev/tools/Makefile.devel
+++ /dev/null
@@ -1,74 +0,0 @@
-# to be linked to makefile (lowercase - takes precedence over Makefile)
-# in main directory
-# make devel in main directory should do this for you.
-
-TOPDIR=.
-BASEDIR=
-
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API
-
-default:	usage noargument
-
-usage::
-	@echo Usage: make \<target\>
-	@echo Targets are:
-
-usage::
-	@echo "  setup-devel	-- set the devel makefile"
-setup-devel:
-	@ln -sfv dev/tools/Makefile.devel makefile
-	@(for i in $(SOURCEDIRS); do \
-	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \
-	done)
-
-
-usage::
-	@echo "  clean-devel	-- clear all devel files"
-clean-devel:
-	echo rm -f makefile .depend.devel
-	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
-
-
-usage::
-	@echo "  coqtop	-- make until the bytecode executable, make the link"
-coqtop:	bin/coqtop.byte
-	ln -sf bin/coqtop.byte coqtop
-
-
-usage::
-	@echo "  quick		-- make bytecode executable and states"
-quick: 
-	$(MAKE) states BEST=byte
-
-include Makefile
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# this file is better described in dev/tools/Makefile.dir
-include .depend.devel
-
-#if dev/tools/Makefile.local exists, it is included
-ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),)
-include $(TOPDIR)/dev/tools/Makefile.local
-endif
-
-
-usage::
-	@echo "  total		-- runs coqtop with all theories required"
-total:
-	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
-
-
-usage::
-	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
-	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
-run:	$(TOPDIR)/coqtop
-	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
-
-
-usage::
-	@echo "  vars		-- echos commands to set COQTOP and COQBIN variables"
-vars:
-	@(cd $(TOPDIR); \
-	echo export COQTOP=`pwd`/ ; \
-	echo export COQBIN=`pwd`/bin/ )
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
deleted file mode 100644
index 1a1bb90b4..000000000
--- a/dev/tools/Makefile.dir
+++ /dev/null
@@ -1,131 +0,0 @@
-# make a link to this file if you are working hard in one directory of Coq
-#   ln -s ../dev/tools/Makefile.dir Makefile
-# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead
-# this Makefile provides many useful facilities to develop Coq
-# it is not completely compatible with .ml4 files unfortunately
-
-ifndef TOPDIR
-TOPDIR=..
-endif
-
-# this complicated thing should work for subsubdirs as well
-BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
-
-noargs:	dir
-
-test-dir:
-	@echo TOPDIR=$(TOPDIR)
-	@echo BASEDIR=$(BASEDIR)
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# make this directory
-dir:
-	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
-
-# make all cmo's in this directory. Useful in case the main Makefile is not
-# up-to-date
-all:	
-	@( ( for i in *.ml; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
-	     done; \
-	     for i in *.ml4; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
-	     done ) \
-	  | xargs $(MAKE) -C $(TOPDIR) )
-
-# lists all files that should be compiled in this directory
-list:
-	@(for i in *.mli; do \
-	   ls -l `basename $$i .mli`.cmi; \
-	done)
-	@(for i in *.ml; do \
-	   ls -l `basename $$i .ml`.cmo; \
-	done)
-	@(for i in *.ml4; do \
-	   ls -l `basename $$i .ml4`.cmo; \
-	done)
-
-
-clean::  
-	rm -f *.cmi *.cmo *.cmx *.o
-
-
-# if grammar.cmo files cannot be compiled and main .depend cannot be
-# rebuilt, this is quite useful
-depend:
-	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
-
-
-# displays the dependency graph of the current directory (vertically,
-# unlike in doc/)
-graph:
-	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
-
-
-# the pretty entry draws a dependency graph marking red those nodes
-# which do not have their .cmo files 
-
-.INTERMEDIATE: depend.dot depend.2.dot
-.PHONY: depend.ps
-
-depend.dot:
-	ocamldep *.ml *.mli | ocamldot > $@
-
-depend.2.dot:	depend.dot
-	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
-	(for ml in *.ml; do \
-	   base=`basename $$ml .ml`; \
-	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
-	   rest=`echo $$base | cut -c2-`; \
-	   name=`echo $$fst $$rest | tr -d " "`; \
-	   cmo=$$base.cmo; \
-	   if [ ! -e $$cmo ]; then \
-	     echo \"$$name\" [color=red]\; >> $@;\
-	   fi;\
-         done;\
-	 echo } >> $@)
-
-depend.ps:	depend.2.dot
-	dot -Tps $< > $@
-
-clean::
-	rm -f depend.ps
-
-pretty:	depend.ps
-	(gv -spartan $<; rm $<) &
-#	gv -spartan $< &
-
-
-
-# generating file.ml.mli by tricking make to pass -i to ocamlc 
-
-%.ml.mli:	FORCE
-	@(cmo=`basename $@ .ml.mli`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
-	echo Generated interface file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-%.annot:	FORCE
-	@(cmo=`basename $@ .annot`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
-	echo Generated annotation file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-FORCE:
-
-clean::
-	rm -f *.ml.mli
-
-# this is not perfect but mostly WORKS! It just calls the main makefile
-
-%.cmi:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-%.cmo:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-coqtop:	
-	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
deleted file mode 100644
index cb914bd12..000000000
--- a/dev/tools/Makefile.subdir
+++ /dev/null
@@ -1,7 +0,0 @@
-# if you work in a sub/sub-rectory of Coq
-# you should make a link to that makefile 
-#    ln -s ../../dev/tools/Makefile.subdir Makefile
-# in order to have all the facilities of dev/tools/Makefile.dir
-
-TOPDIR=../..
-include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/v8-syntax/.gitignore b/dev/v8-syntax/.gitignore
new file mode 100644
index 000000000..89e3509b0
--- /dev/null
+++ b/dev/v8-syntax/.gitignore
@@ -0,0 +1,6 @@
+# byproducts of check-grammar
+def
+df
+use
+use-k
+use-t
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index fa2864cec..6b7960c92 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1158,7 +1158,7 @@ $$
 \nlsep \TERM{Abort}~\NT{ident}
 \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 \nlsep \TERM{Qed}
-\nlsep \TERM{Save}~\NT{ident}}
+\nlsep \TERM{Save}~\NT{ident}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
 \nlsep \TERM{Suspend}
 \nlsep \TERM{Resume}~\OPT{\NT{ident}}