Update lang/coq to 8.3

Main changes:
Includes a new tactic (nsatz, standing for Hilbert's NullStellensatz, that
extends ring to systems of polynomial equations) and a few new libraries (a
certification of mergesort, a new library of finite sets with computational and
logical contents separated).

This version also comes with many improvements of existing features, especially
regarding the tactics, the module system, extraction, the type classes, the
program command, libraries, coqdoc. Here is an excerpt:
* new operator <+ for conveniently chaining application of functors
* new round of extension of the modular library of arithmetic
* support for matching terms with binders in Ltac,
* linking notations in coqdoc,
* quote tactic now working on arbitrary expressions,
* Lemma and co accept parameters that are automatically introduced,
* interactive proofs in module types,
* a beautifying coqc option for pretty-printing files

See the file CHANGES for a full log of changes.

9 files changed, 497 insertions, 423 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index a4af2df7496..c1cda8ca216 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,14 +1,14 @@
-# $NetBSD: Makefile,v 1.26 2010/09/14 11:02:13 wiz Exp $
+# $NetBSD: Makefile,v 1.27 2010/11/14 20:53:02 tonio Exp $
 #
 
-DISTNAME=	coq-8.2pl1
-PKGREVISION=	2
+DISTNAME=	coq-8.3
 CATEGORIES=	lang math
-MASTER_SITES=	http://coq.inria.fr/distrib/V8.2pl1/files/
+MASTER_SITES=	http://coq.inria.fr/distrib/V8.3/files/
 
 MAINTAINER=	richards+netbsd@CS.Princeton.EDU
 HOMEPAGE=	http://coq.inria.fr/
 COMMENT=	Theorem prover which extracts programs from proofs
+LICENSE=	gnu-lgpl-v2.1
 
 PKG_DESTDIR_SUPPORT=	user-destdir
 
@@ -16,7 +16,6 @@ USE_TOOLS+=		gmake
 HAS_CONFIGURE=		YES
 CONFIGURE_ARGS+=	-prefix ${PREFIX}
 CONFIGURE_ARGS+=	-emacslib ${PREFIX}/share/emacs/site-lisp
-CONFIGURE_ARGS+=	-reals all
 BUILD_TARGET=		world
 
 BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=3.10
@@ -28,6 +27,14 @@ BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=3.10
 PLIST_SRC=	${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
 .endif
 
+.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
+.  if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
+      !empty(MACHINE_PLATFORM:MDarwin-*-*) || \
+      !empty(MACHINE_PLATFORM:MFreeBSD-*-*)
+PLIST_SRC+=	${PKGDIR}/PLIST.natdynlink
+.  endif
+.endif
+
 .if ${OPSYS} == "Darwin"
 INSTALL_UNSTRIPPED=	yes
 # See PR# 28772 as the above should work but it appears to be ignored
@@ -37,8 +44,7 @@ _STRIPFLAG_INSTALL=
 .endif
 
 REPLACE_SH=	configure install.sh
-CONFIGURE_ENV+=	SHELL=${SH:Q}
-MAKE_ENV+=	SHELL=${SH:Q}
+INSTALL_ENV+=	COQINSTALLPREFIX=${DESTDIR}
 
 PLIST_VARS=		coqide
 PKG_OPTIONS_VAR=	PKG_OPTIONS.coq
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index 7f1dc99f3d8..253cace0ed9 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,6 +1,4 @@
-@comment $NetBSD: PLIST,v 1.10 2009/09/05 20:44:57 tonio Exp $
-bin/coq-interface
-bin/coq-parser
+@comment $NetBSD: PLIST,v 1.11 2010/11/14 20:53:02 tonio Exp $
 bin/coq-tex
 bin/coq_makefile
 bin/coqc
@@ -8,166 +6,46 @@ bin/coqchk
 bin/coqdep
 bin/coqdoc
 ${PLIST.coqide}bin/coqide
-${PLIST.coqide}bin/coqide.byte
 bin/coqmktop
 bin/coqtop
 bin/coqtop.byte
+${PLIST.coqide}bin/coqide.byte
 bin/coqwc
 bin/gallina
 lib/coq/config/coq_config.cmi
 lib/coq/config/coq_config.cmo
 lib/coq/config/coq_config.cmx
 lib/coq/config/coq_config.o
-lib/coq/contrib/cc/ccalgo.cmi
-lib/coq/contrib/cc/ccproof.cmi
-lib/coq/contrib/cc/cctac.cmi
-lib/coq/contrib/cc/g_congruence.cmi
-lib/coq/contrib/contrib.a
-lib/coq/contrib/contrib.cma
-lib/coq/contrib/contrib.cmxa
-lib/coq/contrib/dp/Dp.vo
-lib/coq/contrib/dp/dp.cmi
-lib/coq/contrib/dp/dp_gappa.cmi
-lib/coq/contrib/dp/dp_why.cmi
-lib/coq/contrib/dp/dp_zenon.cmi
-lib/coq/contrib/dp/g_dp.cmi
-lib/coq/contrib/extraction/common.cmi
-lib/coq/contrib/extraction/extract_env.cmi
-lib/coq/contrib/extraction/extraction.cmi
-lib/coq/contrib/extraction/g_extraction.cmi
-lib/coq/contrib/extraction/haskell.cmi
-lib/coq/contrib/extraction/mlutil.cmi
-lib/coq/contrib/extraction/modutil.cmi
-lib/coq/contrib/extraction/ocaml.cmi
-lib/coq/contrib/extraction/scheme.cmi
-lib/coq/contrib/extraction/table.cmi
-lib/coq/contrib/field/LegacyField.vo
-lib/coq/contrib/field/LegacyField_Compl.vo
-lib/coq/contrib/field/LegacyField_Tactic.vo
-lib/coq/contrib/field/LegacyField_Theory.vo
-lib/coq/contrib/field/field.cmi
-lib/coq/contrib/firstorder/formula.cmi
-lib/coq/contrib/firstorder/g_ground.cmi
-lib/coq/contrib/firstorder/ground.cmi
-lib/coq/contrib/firstorder/instances.cmi
-lib/coq/contrib/firstorder/rules.cmi
-lib/coq/contrib/firstorder/sequent.cmi
-lib/coq/contrib/firstorder/unify.cmi
-lib/coq/contrib/fourier/Fourier.vo
-lib/coq/contrib/fourier/Fourier_util.vo
-lib/coq/contrib/fourier/fourier.cmi
-lib/coq/contrib/fourier/fourierR.cmi
-lib/coq/contrib/fourier/g_fourier.cmi
-lib/coq/contrib/funind/Recdef.vo
-lib/coq/contrib/funind/functional_principles_proofs.cmi
-lib/coq/contrib/funind/functional_principles_types.cmi
-lib/coq/contrib/funind/g_indfun.cmi
-lib/coq/contrib/funind/indfun.cmi
-lib/coq/contrib/funind/indfun_common.cmi
-lib/coq/contrib/funind/invfun.cmi
-lib/coq/contrib/funind/merge.cmi
-lib/coq/contrib/funind/rawterm_to_relation.cmi
-lib/coq/contrib/funind/rawtermops.cmi
-lib/coq/contrib/funind/recdef.cmi
-lib/coq/contrib/interface/vernacrc
-lib/coq/contrib/micromega/CheckerMaker.vo
-lib/coq/contrib/micromega/Env.vo
-lib/coq/contrib/micromega/EnvRing.vo
-lib/coq/contrib/micromega/OrderedRing.vo
-lib/coq/contrib/micromega/Psatz.vo
-lib/coq/contrib/micromega/QMicromega.vo
-lib/coq/contrib/micromega/RMicromega.vo
-lib/coq/contrib/micromega/Refl.vo
-lib/coq/contrib/micromega/RingMicromega.vo
-lib/coq/contrib/micromega/Tauto.vo
-lib/coq/contrib/micromega/VarMap.vo
-lib/coq/contrib/micromega/ZCoeff.vo
-lib/coq/contrib/micromega/ZMicromega.vo
-lib/coq/contrib/micromega/certificate.cmi
-lib/coq/contrib/micromega/coq_micromega.cmi
-lib/coq/contrib/micromega/csdpcert
-lib/coq/contrib/micromega/g_micromega.cmi
-lib/coq/contrib/micromega/mfourier.cmi
-lib/coq/contrib/micromega/micromega.cmi
-lib/coq/contrib/micromega/mutils.cmi
-lib/coq/contrib/micromega/vector.cmi
-lib/coq/contrib/omega/Omega.vo
-lib/coq/contrib/omega/OmegaLemmas.vo
-lib/coq/contrib/omega/PreOmega.vo
-lib/coq/contrib/omega/coq_omega.cmi
-lib/coq/contrib/omega/g_omega.cmi
-lib/coq/contrib/omega/omega.cmi
-lib/coq/contrib/ring/LegacyArithRing.vo
-lib/coq/contrib/ring/LegacyNArithRing.vo
-lib/coq/contrib/ring/LegacyRing.vo
-lib/coq/contrib/ring/LegacyRing_theory.vo
-lib/coq/contrib/ring/LegacyZArithRing.vo
-lib/coq/contrib/ring/Quote.vo
-lib/coq/contrib/ring/Ring_abstract.vo
-lib/coq/contrib/ring/Ring_normalize.vo
-lib/coq/contrib/ring/Setoid_ring.vo
-lib/coq/contrib/ring/Setoid_ring_normalize.vo
-lib/coq/contrib/ring/Setoid_ring_theory.vo
-lib/coq/contrib/ring/g_quote.cmi
-lib/coq/contrib/ring/g_ring.cmi
-lib/coq/contrib/ring/quote.cmi
-lib/coq/contrib/ring/ring.cmi
-lib/coq/contrib/romega/ROmega.vo
-lib/coq/contrib/romega/ReflOmegaCore.vo
-lib/coq/contrib/romega/const_omega.cmi
-lib/coq/contrib/romega/g_romega.cmi
-lib/coq/contrib/romega/refl_omega.cmi
-lib/coq/contrib/rtauto/Bintree.vo
-lib/coq/contrib/rtauto/Rtauto.vo
-lib/coq/contrib/rtauto/g_rtauto.cmi
-lib/coq/contrib/rtauto/proof_search.cmi
-lib/coq/contrib/rtauto/refl_tauto.cmi
-lib/coq/contrib/setoid_ring/ArithRing.vo
-lib/coq/contrib/setoid_ring/BinList.vo
-lib/coq/contrib/setoid_ring/Field.vo
-lib/coq/contrib/setoid_ring/Field_tac.vo
-lib/coq/contrib/setoid_ring/Field_theory.vo
-lib/coq/contrib/setoid_ring/InitialRing.vo
-lib/coq/contrib/setoid_ring/NArithRing.vo
-lib/coq/contrib/setoid_ring/RealField.vo
-lib/coq/contrib/setoid_ring/Ring.vo
-lib/coq/contrib/setoid_ring/Ring_base.vo
-lib/coq/contrib/setoid_ring/Ring_equiv.vo
-lib/coq/contrib/setoid_ring/Ring_polynom.vo
-lib/coq/contrib/setoid_ring/Ring_tac.vo
-lib/coq/contrib/setoid_ring/Ring_theory.vo
-lib/coq/contrib/setoid_ring/ZArithRing.vo
-lib/coq/contrib/setoid_ring/newring.cmi
-lib/coq/contrib/subtac/equations.cmi
-lib/coq/contrib/subtac/eterm.cmi
-lib/coq/contrib/subtac/g_eterm.cmi
-lib/coq/contrib/subtac/g_subtac.cmi
-lib/coq/contrib/subtac/subtac.cmi
-lib/coq/contrib/subtac/subtac_cases.cmi
-lib/coq/contrib/subtac/subtac_classes.cmi
-lib/coq/contrib/subtac/subtac_coercion.cmi
-lib/coq/contrib/subtac/subtac_command.cmi
-lib/coq/contrib/subtac/subtac_errors.cmi
-lib/coq/contrib/subtac/subtac_obligations.cmi
-lib/coq/contrib/subtac/subtac_pretyping.cmi
-lib/coq/contrib/subtac/subtac_pretyping_F.cmi
-lib/coq/contrib/subtac/subtac_utils.cmi
-lib/coq/contrib/xml/acic.cmi
-lib/coq/contrib/xml/acic2Xml.cmi
-lib/coq/contrib/xml/cic2Xml.cmi
-lib/coq/contrib/xml/cic2acic.cmi
-lib/coq/contrib/xml/doubleTypeInference.cmi
-lib/coq/contrib/xml/dumptree.cmi
-lib/coq/contrib/xml/proof2aproof.cmi
-lib/coq/contrib/xml/proofTree2Xml.cmi
-lib/coq/contrib/xml/unshare.cmi
-lib/coq/contrib/xml/xml.cmi
-lib/coq/contrib/xml/xmlcommand.cmi
-lib/coq/contrib/xml/xmlentries.cmi
 lib/coq/dllcoqrun.so
 lib/coq/ide/.coqide-gtk2rc
 lib/coq/ide/FAQ
+${PLIST.coqide}lib/coq/ide/command_windows.cmi
+${PLIST.coqide}lib/coq/ide/config_lexer.cmi
+${PLIST.coqide}lib/coq/ide/config_parser.cmi
+${PLIST.coqide}lib/coq/ide/coq.cmi
 lib/coq/ide/coq.png
+${PLIST.coqide}lib/coq/ide/coq_commands.cmi
+${PLIST.coqide}lib/coq/ide/coq_lex.cmi
+${PLIST.coqide}lib/coq/ide/coq_tactics.cmi
+${PLIST.coqide}lib/coq/ide/coqide.cmi
+${PLIST.coqide}lib/coq/ide/gtk_parsing.cmi
+${PLIST.coqide}lib/coq/ide/ide.a
+${PLIST.coqide}lib/coq/ide/ide.cma
+${PLIST.coqide}lib/coq/ide/ide.cmxa
+${PLIST.coqide}lib/coq/ide/ideutils.cmi
+${PLIST.coqide}lib/coq/ide/preferences.cmi
+${PLIST.coqide}lib/coq/ide/tags.cmi
+${PLIST.coqide}lib/coq/ide/typed_notebook.cmi
+${PLIST.coqide}lib/coq/ide/undo.cmi
+${PLIST.coqide}lib/coq/ide/utf8_convert.cmi
+${PLIST.coqide}lib/coq/ide/utils/config_file.cmi
+${PLIST.coqide}lib/coq/ide/utils/configwin.cmi
+${PLIST.coqide}lib/coq/ide/utils/configwin_ihm.cmi
+${PLIST.coqide}lib/coq/ide/utils/configwin_keys.cmi
+${PLIST.coqide}lib/coq/ide/utils/configwin_messages.cmi
+${PLIST.coqide}lib/coq/ide/utils/configwin_types.cmi
+${PLIST.coqide}lib/coq/ide/utils/editable_cells.cmi
+${PLIST.coqide}lib/coq/ide/utils/okey.cmi
 lib/coq/interp/constrextern.cmi
 lib/coq/interp/constrintern.cmi
 lib/coq/interp/coqlib.cmi
@@ -181,6 +59,7 @@ lib/coq/interp/modintern.cmi
 lib/coq/interp/notation.cmi
 lib/coq/interp/ppextend.cmi
 lib/coq/interp/reserve.cmi
+lib/coq/interp/smartlocate.cmi
 lib/coq/interp/syntax_def.cmi
 lib/coq/interp/topconstr.cmi
 lib/coq/kernel/cbytecodes.cmi
@@ -220,11 +99,14 @@ lib/coq/kernel/vm.cmi
 lib/coq/lib/bigint.cmi
 lib/coq/lib/bstack.cmi
 lib/coq/lib/compat.cmi
+lib/coq/lib/dnet.cmi
 lib/coq/lib/dyn.cmi
 lib/coq/lib/edit.cmi
 lib/coq/lib/envars.cmi
 lib/coq/lib/explore.cmi
 lib/coq/lib/flags.cmi
+lib/coq/lib/fmap.cmi
+lib/coq/lib/fset.cmi
 lib/coq/lib/gmap.cmi
 lib/coq/lib/gmapl.cmi
 lib/coq/lib/gset.cmi
@@ -239,8 +121,11 @@ lib/coq/lib/pp_control.cmi
 lib/coq/lib/predicate.cmi
 lib/coq/lib/profile.cmi
 lib/coq/lib/rtree.cmi
+lib/coq/lib/segmenttree.cmi
 lib/coq/lib/system.cmi
 lib/coq/lib/tlm.cmi
+lib/coq/lib/tries.cmi
+lib/coq/lib/unicodetable.cmi
 lib/coq/lib/util.cmi
 lib/coq/libcoqrun.a
 lib/coq/library/decl_kinds.cmi
@@ -265,20 +150,15 @@ lib/coq/library/states.cmi
 lib/coq/library/summary.cmi
 lib/coq/parsing/egrammar.cmi
 lib/coq/parsing/extend.cmi
-lib/coq/parsing/g_ascii_syntax.cmi
+lib/coq/parsing/extrawit.cmi
 lib/coq/parsing/g_constr.cmi
 lib/coq/parsing/g_decl_mode.cmi
-lib/coq/parsing/g_intsyntax.cmi
 lib/coq/parsing/g_ltac.cmi
-lib/coq/parsing/g_natsyntax.cmi
 lib/coq/parsing/g_prim.cmi
 lib/coq/parsing/g_proofs.cmi
-lib/coq/parsing/g_rsyntax.cmi
-lib/coq/parsing/g_string_syntax.cmi
 lib/coq/parsing/g_tactic.cmi
 lib/coq/parsing/g_vernac.cmi
 lib/coq/parsing/g_xml.cmi
-lib/coq/parsing/g_zsyntax.cmi
 lib/coq/parsing/grammar.cma
 lib/coq/parsing/highparsing.a
 lib/coq/parsing/highparsing.cma
@@ -295,8 +175,259 @@ lib/coq/parsing/ppvernac.cmi
 lib/coq/parsing/prettyp.cmi
 lib/coq/parsing/printer.cmi
 lib/coq/parsing/printmod.cmi
-lib/coq/parsing/search.cmi
 lib/coq/parsing/tactic_printer.cmi
+lib/coq/plugins/cc/cc_plugin.a
+lib/coq/plugins/cc/cc_plugin.cma
+lib/coq/plugins/cc/cc_plugin.cmxa
+lib/coq/plugins/cc/cc_plugin_mod.cmi
+lib/coq/plugins/cc/ccalgo.cmi
+lib/coq/plugins/cc/ccproof.cmi
+lib/coq/plugins/cc/cctac.cmi
+lib/coq/plugins/cc/g_congruence.cmi
+lib/coq/plugins/dp/Dp.vo
+lib/coq/plugins/dp/dp.cmi
+lib/coq/plugins/dp/dp_plugin.a
+lib/coq/plugins/dp/dp_plugin.cma
+lib/coq/plugins/dp/dp_plugin.cmxa
+lib/coq/plugins/dp/dp_plugin_mod.cmi
+lib/coq/plugins/dp/dp_why.cmi
+lib/coq/plugins/dp/dp_zenon.cmi
+lib/coq/plugins/dp/g_dp.cmi
+lib/coq/plugins/extraction/ExtrOcamlBasic.vo
+lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
+lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
+lib/coq/plugins/extraction/ExtrOcamlNatBigInt.vo
+lib/coq/plugins/extraction/ExtrOcamlNatInt.vo
+lib/coq/plugins/extraction/ExtrOcamlString.vo
+lib/coq/plugins/extraction/ExtrOcamlZBigInt.vo
+lib/coq/plugins/extraction/ExtrOcamlZInt.vo
+lib/coq/plugins/extraction/common.cmi
+lib/coq/plugins/extraction/extract_env.cmi
+lib/coq/plugins/extraction/extraction.cmi
+lib/coq/plugins/extraction/extraction_plugin.a
+lib/coq/plugins/extraction/extraction_plugin.cma
+lib/coq/plugins/extraction/extraction_plugin.cmxa
+lib/coq/plugins/extraction/extraction_plugin_mod.cmi
+lib/coq/plugins/extraction/g_extraction.cmi
+lib/coq/plugins/extraction/haskell.cmi
+lib/coq/plugins/extraction/mlutil.cmi
+lib/coq/plugins/extraction/modutil.cmi
+lib/coq/plugins/extraction/ocaml.cmi
+lib/coq/plugins/extraction/scheme.cmi
+lib/coq/plugins/extraction/table.cmi
+lib/coq/plugins/field/LegacyField.vo
+lib/coq/plugins/field/LegacyField_Compl.vo
+lib/coq/plugins/field/LegacyField_Tactic.vo
+lib/coq/plugins/field/LegacyField_Theory.vo
+lib/coq/plugins/field/field.cmi
+lib/coq/plugins/field/field_plugin.a
+lib/coq/plugins/field/field_plugin.cma
+lib/coq/plugins/field/field_plugin.cmxa
+lib/coq/plugins/field/field_plugin_mod.cmi
+lib/coq/plugins/firstorder/formula.cmi
+lib/coq/plugins/firstorder/g_ground.cmi
+lib/coq/plugins/firstorder/ground.cmi
+lib/coq/plugins/firstorder/ground_plugin.a
+lib/coq/plugins/firstorder/ground_plugin.cma
+lib/coq/plugins/firstorder/ground_plugin.cmxa
+lib/coq/plugins/firstorder/ground_plugin_mod.cmi
+lib/coq/plugins/firstorder/instances.cmi
+lib/coq/plugins/firstorder/rules.cmi
+lib/coq/plugins/firstorder/sequent.cmi
+lib/coq/plugins/firstorder/unify.cmi
+lib/coq/plugins/fourier/Fourier.vo
+lib/coq/plugins/fourier/Fourier_util.vo
+lib/coq/plugins/fourier/fourier.cmi
+lib/coq/plugins/fourier/fourierR.cmi
+lib/coq/plugins/fourier/fourier_plugin.a
+lib/coq/plugins/fourier/fourier_plugin.cma
+lib/coq/plugins/fourier/fourier_plugin.cmxa
+lib/coq/plugins/fourier/fourier_plugin_mod.cmi
+lib/coq/plugins/fourier/g_fourier.cmi
+lib/coq/plugins/funind/Recdef.vo
+lib/coq/plugins/funind/functional_principles_proofs.cmi
+lib/coq/plugins/funind/functional_principles_types.cmi
+lib/coq/plugins/funind/g_indfun.cmi
+lib/coq/plugins/funind/indfun.cmi
+lib/coq/plugins/funind/indfun_common.cmi
+lib/coq/plugins/funind/invfun.cmi
+lib/coq/plugins/funind/merge.cmi
+lib/coq/plugins/funind/rawterm_to_relation.cmi
+lib/coq/plugins/funind/rawtermops.cmi
+lib/coq/plugins/funind/recdef.cmi
+lib/coq/plugins/funind/recdef_plugin.a
+lib/coq/plugins/funind/recdef_plugin.cma
+lib/coq/plugins/funind/recdef_plugin.cmxa
+lib/coq/plugins/funind/recdef_plugin_mod.cmi
+lib/coq/plugins/micromega/CheckerMaker.vo
+lib/coq/plugins/micromega/Env.vo
+lib/coq/plugins/micromega/EnvRing.vo
+lib/coq/plugins/micromega/OrderedRing.vo
+lib/coq/plugins/micromega/Psatz.vo
+lib/coq/plugins/micromega/QMicromega.vo
+lib/coq/plugins/micromega/RMicromega.vo
+lib/coq/plugins/micromega/Refl.vo
+lib/coq/plugins/micromega/RingMicromega.vo
+lib/coq/plugins/micromega/Tauto.vo
+lib/coq/plugins/micromega/VarMap.vo
+lib/coq/plugins/micromega/ZCoeff.vo
+lib/coq/plugins/micromega/ZMicromega.vo
+lib/coq/plugins/micromega/certificate.cmi
+lib/coq/plugins/micromega/coq_micromega.cmi
+lib/coq/plugins/micromega/csdpcert
+lib/coq/plugins/micromega/g_micromega.cmi
+lib/coq/plugins/micromega/mfourier.cmi
+lib/coq/plugins/micromega/micromega.cmi
+lib/coq/plugins/micromega/micromega_plugin.a
+lib/coq/plugins/micromega/micromega_plugin.cma
+lib/coq/plugins/micromega/micromega_plugin.cmxa
+lib/coq/plugins/micromega/micromega_plugin_mod.cmi
+lib/coq/plugins/micromega/mutils.cmi
+lib/coq/plugins/micromega/persistent_cache.cmi
+lib/coq/plugins/micromega/sos_types.cmi
+lib/coq/plugins/nsatz/Nsatz.vo
+lib/coq/plugins/nsatz/ideal.cmi
+lib/coq/plugins/nsatz/nsatz.cmi
+lib/coq/plugins/nsatz/nsatz_plugin.a
+lib/coq/plugins/nsatz/nsatz_plugin.cma
+lib/coq/plugins/nsatz/nsatz_plugin.cmxa
+lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
+lib/coq/plugins/nsatz/polynom.cmi
+lib/coq/plugins/nsatz/utile.cmi
+lib/coq/plugins/omega/Omega.vo
+lib/coq/plugins/omega/OmegaLemmas.vo
+lib/coq/plugins/omega/OmegaPlugin.vo
+lib/coq/plugins/omega/PreOmega.vo
+lib/coq/plugins/omega/coq_omega.cmi
+lib/coq/plugins/omega/g_omega.cmi
+lib/coq/plugins/omega/omega.cmi
+lib/coq/plugins/omega/omega_plugin.a
+lib/coq/plugins/omega/omega_plugin.cma
+lib/coq/plugins/omega/omega_plugin.cmxa
+lib/coq/plugins/omega/omega_plugin_mod.cmi
+lib/coq/plugins/quote/Quote.vo
+lib/coq/plugins/quote/g_quote.cmi
+lib/coq/plugins/quote/quote.cmi
+lib/coq/plugins/quote/quote_plugin.a
+lib/coq/plugins/quote/quote_plugin.cma
+lib/coq/plugins/quote/quote_plugin.cmxa
+lib/coq/plugins/quote/quote_plugin_mod.cmi
+lib/coq/plugins/ring/LegacyArithRing.vo
+lib/coq/plugins/ring/LegacyNArithRing.vo
+lib/coq/plugins/ring/LegacyRing.vo
+lib/coq/plugins/ring/LegacyRing_theory.vo
+lib/coq/plugins/ring/LegacyZArithRing.vo
+lib/coq/plugins/ring/Ring_abstract.vo
+lib/coq/plugins/ring/Ring_normalize.vo
+lib/coq/plugins/ring/Setoid_ring.vo
+lib/coq/plugins/ring/Setoid_ring_normalize.vo
+lib/coq/plugins/ring/Setoid_ring_theory.vo
+lib/coq/plugins/ring/g_ring.cmi
+lib/coq/plugins/ring/ring.cmi
+lib/coq/plugins/ring/ring_plugin.a
+lib/coq/plugins/ring/ring_plugin.cma
+lib/coq/plugins/ring/ring_plugin.cmxa
+lib/coq/plugins/ring/ring_plugin_mod.cmi
+lib/coq/plugins/romega/ROmega.vo
+lib/coq/plugins/romega/ReflOmegaCore.vo
+lib/coq/plugins/romega/const_omega.cmi
+lib/coq/plugins/romega/g_romega.cmi
+lib/coq/plugins/romega/refl_omega.cmi
+lib/coq/plugins/romega/romega_plugin.a
+lib/coq/plugins/romega/romega_plugin.cma
+lib/coq/plugins/romega/romega_plugin.cmxa
+lib/coq/plugins/romega/romega_plugin_mod.cmi
+lib/coq/plugins/rtauto/Bintree.vo
+lib/coq/plugins/rtauto/Rtauto.vo
+lib/coq/plugins/rtauto/g_rtauto.cmi
+lib/coq/plugins/rtauto/proof_search.cmi
+lib/coq/plugins/rtauto/refl_tauto.cmi
+lib/coq/plugins/rtauto/rtauto_plugin.a
+lib/coq/plugins/rtauto/rtauto_plugin.cma
+lib/coq/plugins/rtauto/rtauto_plugin.cmxa
+lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
+lib/coq/plugins/setoid_ring/ArithRing.vo
+lib/coq/plugins/setoid_ring/BinList.vo
+lib/coq/plugins/setoid_ring/Field.vo
+lib/coq/plugins/setoid_ring/Field_tac.vo
+lib/coq/plugins/setoid_ring/Field_theory.vo
+lib/coq/plugins/setoid_ring/InitialRing.vo
+lib/coq/plugins/setoid_ring/NArithRing.vo
+lib/coq/plugins/setoid_ring/RealField.vo
+lib/coq/plugins/setoid_ring/Ring.vo
+lib/coq/plugins/setoid_ring/Ring_base.vo
+lib/coq/plugins/setoid_ring/Ring_equiv.vo
+lib/coq/plugins/setoid_ring/Ring_polynom.vo
+lib/coq/plugins/setoid_ring/Ring_tac.vo
+lib/coq/plugins/setoid_ring/Ring_theory.vo
+lib/coq/plugins/setoid_ring/ZArithRing.vo
+lib/coq/plugins/setoid_ring/newring.cmi
+lib/coq/plugins/setoid_ring/newring_plugin.a
+lib/coq/plugins/setoid_ring/newring_plugin.cma
+lib/coq/plugins/setoid_ring/newring_plugin.cmxa
+lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
+lib/coq/plugins/subtac/eterm.cmi
+lib/coq/plugins/subtac/g_subtac.cmi
+lib/coq/plugins/subtac/subtac.cmi
+lib/coq/plugins/subtac/subtac_cases.cmi
+lib/coq/plugins/subtac/subtac_classes.cmi
+lib/coq/plugins/subtac/subtac_coercion.cmi
+lib/coq/plugins/subtac/subtac_command.cmi
+lib/coq/plugins/subtac/subtac_errors.cmi
+lib/coq/plugins/subtac/subtac_obligations.cmi
+lib/coq/plugins/subtac/subtac_plugin.a
+lib/coq/plugins/subtac/subtac_plugin.cma
+lib/coq/plugins/subtac/subtac_plugin.cmxa
+lib/coq/plugins/subtac/subtac_plugin_mod.cmi
+lib/coq/plugins/subtac/subtac_pretyping.cmi
+lib/coq/plugins/subtac/subtac_pretyping_F.cmi
+lib/coq/plugins/subtac/subtac_utils.cmi
+lib/coq/plugins/syntax/ascii_syntax.cmi
+lib/coq/plugins/syntax/ascii_syntax_plugin.a
+lib/coq/plugins/syntax/ascii_syntax_plugin.cma
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmxa
+lib/coq/plugins/syntax/ascii_syntax_plugin_mod.cmi
+lib/coq/plugins/syntax/nat_syntax.cmi
+lib/coq/plugins/syntax/nat_syntax_plugin.a
+lib/coq/plugins/syntax/nat_syntax_plugin.cma
+lib/coq/plugins/syntax/nat_syntax_plugin.cmxa
+lib/coq/plugins/syntax/nat_syntax_plugin_mod.cmi
+lib/coq/plugins/syntax/numbers_syntax.cmi
+lib/coq/plugins/syntax/numbers_syntax_plugin.a
+lib/coq/plugins/syntax/numbers_syntax_plugin.cma
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmxa
+lib/coq/plugins/syntax/numbers_syntax_plugin_mod.cmi
+lib/coq/plugins/syntax/r_syntax.cmi
+lib/coq/plugins/syntax/r_syntax_plugin.a
+lib/coq/plugins/syntax/r_syntax_plugin.cma
+lib/coq/plugins/syntax/r_syntax_plugin.cmxa
+lib/coq/plugins/syntax/r_syntax_plugin_mod.cmi
+lib/coq/plugins/syntax/string_syntax.cmi
+lib/coq/plugins/syntax/string_syntax_plugin.a
+lib/coq/plugins/syntax/string_syntax_plugin.cma
+lib/coq/plugins/syntax/string_syntax_plugin.cmxa
+lib/coq/plugins/syntax/string_syntax_plugin_mod.cmi
+lib/coq/plugins/syntax/z_syntax.cmi
+lib/coq/plugins/syntax/z_syntax_plugin.a
+lib/coq/plugins/syntax/z_syntax_plugin.cma
+lib/coq/plugins/syntax/z_syntax_plugin.cmxa
+lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
+lib/coq/plugins/xml/acic.cmi
+lib/coq/plugins/xml/acic2Xml.cmi
+lib/coq/plugins/xml/cic2Xml.cmi
+lib/coq/plugins/xml/cic2acic.cmi
+lib/coq/plugins/xml/doubleTypeInference.cmi
+lib/coq/plugins/xml/dumptree.cmi
+lib/coq/plugins/xml/proof2aproof.cmi
+lib/coq/plugins/xml/proofTree2Xml.cmi
+lib/coq/plugins/xml/unshare.cmi
+lib/coq/plugins/xml/xml.cmi
+lib/coq/plugins/xml/xml_plugin.a
+lib/coq/plugins/xml/xml_plugin.cma
+lib/coq/plugins/xml/xml_plugin.cmxa
+lib/coq/plugins/xml/xml_plugin_mod.cmi
+lib/coq/plugins/xml/xmlcommand.cmi
+lib/coq/plugins/xml/xmlentries.cmi
 lib/coq/pretyping/cases.cmi
 lib/coq/pretyping/cbv.cmi
 lib/coq/pretyping/classops.cmi
@@ -309,6 +440,7 @@ lib/coq/pretyping/evd.cmi
 lib/coq/pretyping/indrec.cmi
 lib/coq/pretyping/inductiveops.cmi
 lib/coq/pretyping/matching.cmi
+lib/coq/pretyping/namegen.cmi
 lib/coq/pretyping/pattern.cmi
 lib/coq/pretyping/pretype_errors.cmi
 lib/coq/pretyping/pretyping.a
@@ -320,6 +452,7 @@ lib/coq/pretyping/recordops.cmi
 lib/coq/pretyping/reductionops.cmi
 lib/coq/pretyping/retyping.cmi
 lib/coq/pretyping/tacred.cmi
+lib/coq/pretyping/term_dnet.cmi
 lib/coq/pretyping/termops.cmi
 lib/coq/pretyping/typeclasses.cmi
 lib/coq/pretyping/typeclasses_errors.cmi
@@ -353,7 +486,9 @@ lib/coq/tactics/dhyp.cmi
 lib/coq/tactics/dn.cmi
 lib/coq/tactics/eauto.cmi
 lib/coq/tactics/elim.cmi
+lib/coq/tactics/elimschemes.cmi
 lib/coq/tactics/eqdecide.cmi
+lib/coq/tactics/eqschemes.cmi
 lib/coq/tactics/equality.cmi
 lib/coq/tactics/evar_tactics.cmi
 lib/coq/tactics/extraargs.cmi
@@ -367,7 +502,9 @@ lib/coq/tactics/inv.cmi
 lib/coq/tactics/leminv.cmi
 lib/coq/tactics/nbtermdn.cmi
 lib/coq/tactics/refine.cmi
+lib/coq/tactics/rewrite.cmi
 lib/coq/tactics/tacinterp.cmi
+lib/coq/tactics/tactic_option.cmi
 lib/coq/tactics/tacticals.cmi
 lib/coq/tactics/tactics.a
 lib/coq/tactics/tactics.cma
@@ -391,8 +528,10 @@ lib/coq/theories/Arith/Le.vo
 lib/coq/theories/Arith/Lt.vo
 lib/coq/theories/Arith/Max.vo
 lib/coq/theories/Arith/Min.vo
+lib/coq/theories/Arith/MinMax.vo
 lib/coq/theories/Arith/Minus.vo
 lib/coq/theories/Arith/Mult.vo
+lib/coq/theories/Arith/NatOrderedType.vo
 lib/coq/theories/Arith/Peano_dec.vo
 lib/coq/theories/Arith/Plus.vo
 lib/coq/theories/Arith/Wf_nat.vo
@@ -405,13 +544,12 @@ lib/coq/theories/Bool/Sumbool.vo
 lib/coq/theories/Bool/Zerob.vo
 lib/coq/theories/Classes/EquivDec.vo
 lib/coq/theories/Classes/Equivalence.vo
-lib/coq/theories/Classes/Functions.vo
 lib/coq/theories/Classes/Init.vo
 lib/coq/theories/Classes/Morphisms.vo
 lib/coq/theories/Classes/Morphisms_Prop.vo
 lib/coq/theories/Classes/Morphisms_Relations.vo
 lib/coq/theories/Classes/RelationClasses.vo
-lib/coq/theories/Classes/SetoidAxioms.vo
+lib/coq/theories/Classes/RelationPairs.vo
 lib/coq/theories/Classes/SetoidClass.vo
 lib/coq/theories/Classes/SetoidDec.vo
 lib/coq/theories/Classes/SetoidTactics.vo
@@ -425,19 +563,17 @@ lib/coq/theories/FSets/FMapWeakList.vo
 lib/coq/theories/FSets/FMaps.vo
 lib/coq/theories/FSets/FSetAVL.vo
 lib/coq/theories/FSets/FSetBridge.vo
+lib/coq/theories/FSets/FSetCompat.vo
 lib/coq/theories/FSets/FSetDecide.vo
 lib/coq/theories/FSets/FSetEqProperties.vo
 lib/coq/theories/FSets/FSetFacts.vo
-lib/coq/theories/FSets/FSetFullAVL.vo
 lib/coq/theories/FSets/FSetInterface.vo
 lib/coq/theories/FSets/FSetList.vo
+lib/coq/theories/FSets/FSetPositive.vo
 lib/coq/theories/FSets/FSetProperties.vo
 lib/coq/theories/FSets/FSetToFiniteSet.vo
 lib/coq/theories/FSets/FSetWeakList.vo
 lib/coq/theories/FSets/FSets.vo
-lib/coq/theories/FSets/OrderedType.vo
-lib/coq/theories/FSets/OrderedTypeAlt.vo
-lib/coq/theories/FSets/OrderedTypeEx.vo
 lib/coq/theories/Init/Datatypes.vo
 lib/coq/theories/Init/Logic.vo
 lib/coq/theories/Init/Logic_Type.vo
@@ -450,7 +586,6 @@ lib/coq/theories/Init/Wf.vo
 lib/coq/theories/Lists/List.vo
 lib/coq/theories/Lists/ListSet.vo
 lib/coq/theories/Lists/ListTactics.vo
-lib/coq/theories/Lists/MonoList.vo
 lib/coq/theories/Lists/SetoidList.vo
 lib/coq/theories/Lists/StreamMemo.vo
 lib/coq/theories/Lists/Streams.vo
@@ -469,8 +604,6 @@ lib/coq/theories/Logic/Classical_Prop.vo
 lib/coq/theories/Logic/Classical_Type.vo
 lib/coq/theories/Logic/ConstructiveEpsilon.vo
 lib/coq/theories/Logic/Decidable.vo
-lib/coq/theories/Logic/DecidableType.vo
-lib/coq/theories/Logic/DecidableTypeEx.vo
 lib/coq/theories/Logic/Description.vo
 lib/coq/theories/Logic/Diaconescu.vo
 lib/coq/theories/Logic/Epsilon.vo
@@ -485,13 +618,28 @@ lib/coq/theories/Logic/ProofIrrelevance.vo
 lib/coq/theories/Logic/ProofIrrelevanceFacts.vo
 lib/coq/theories/Logic/RelationalChoice.vo
 lib/coq/theories/Logic/SetIsType.vo
+lib/coq/theories/MSets/MSetAVL.vo
+lib/coq/theories/MSets/MSetDecide.vo
+lib/coq/theories/MSets/MSetEqProperties.vo
+lib/coq/theories/MSets/MSetFacts.vo
+lib/coq/theories/MSets/MSetInterface.vo
+lib/coq/theories/MSets/MSetList.vo
+lib/coq/theories/MSets/MSetPositive.vo
+lib/coq/theories/MSets/MSetProperties.vo
+lib/coq/theories/MSets/MSetToFiniteSet.vo
+lib/coq/theories/MSets/MSetWeakList.vo
+lib/coq/theories/MSets/MSets.vo
 lib/coq/theories/NArith/BinNat.vo
 lib/coq/theories/NArith/BinPos.vo
 lib/coq/theories/NArith/NArith.vo
+lib/coq/theories/NArith/NOrderedType.vo
 lib/coq/theories/NArith/Ndec.vo
 lib/coq/theories/NArith/Ndigits.vo
 lib/coq/theories/NArith/Ndist.vo
+lib/coq/theories/NArith/Nminmax.vo
 lib/coq/theories/NArith/Nnat.vo
+lib/coq/theories/NArith/POrderedType.vo
+lib/coq/theories/NArith/Pminmax.vo
 lib/coq/theories/NArith/Pnat.vo
 lib/coq/theories/Numbers/BigNumPrelude.vo
 lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
@@ -508,14 +656,20 @@ lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.vo
 lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.vo
 lib/coq/theories/Numbers/Cyclic/Int31/Cyclic31.vo
 lib/coq/theories/Numbers/Cyclic/Int31/Int31.vo
+lib/coq/theories/Numbers/Cyclic/Int31/Ring31.vo
 lib/coq/theories/Numbers/Cyclic/ZModulo/ZModulo.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZAdd.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZBase.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZDivEucl.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo
 lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo
 lib/coq/theories/Numbers/Integer/BigZ/BigZ.vo
 lib/coq/theories/Numbers/Integer/BigZ/ZMake.vo
 lib/coq/theories/Numbers/Integer/Binary/ZBinary.vo
@@ -527,22 +681,28 @@ lib/coq/theories/Numbers/NatInt/NZAdd.vo
 lib/coq/theories/Numbers/NatInt/NZAddOrder.vo
 lib/coq/theories/Numbers/NatInt/NZAxioms.vo
 lib/coq/theories/Numbers/NatInt/NZBase.vo
+lib/coq/theories/Numbers/NatInt/NZDiv.vo
+lib/coq/theories/Numbers/NatInt/NZDomain.vo
 lib/coq/theories/Numbers/NatInt/NZMul.vo
 lib/coq/theories/Numbers/NatInt/NZMulOrder.vo
 lib/coq/theories/Numbers/NatInt/NZOrder.vo
+lib/coq/theories/Numbers/NatInt/NZProperties.vo
 lib/coq/theories/Numbers/Natural/Abstract/NAdd.vo
 lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo
 lib/coq/theories/Numbers/Natural/Abstract/NAxioms.vo
 lib/coq/theories/Numbers/Natural/Abstract/NBase.vo
+lib/coq/theories/Numbers/Natural/Abstract/NDefOps.vo
+lib/coq/theories/Numbers/Natural/Abstract/NDiv.vo
 lib/coq/theories/Numbers/Natural/Abstract/NIso.vo
-lib/coq/theories/Numbers/Natural/Abstract/NMul.vo
 lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
 lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NProperties.vo
+lib/coq/theories/Numbers/Natural/Abstract/NStrongRec.vo
 lib/coq/theories/Numbers/Natural/Abstract/NSub.vo
 lib/coq/theories/Numbers/Natural/BigN/BigN.vo
 lib/coq/theories/Numbers/Natural/BigN/NMake.vo
+lib/coq/theories/Numbers/Natural/BigN/NMake_gen.vo
 lib/coq/theories/Numbers/Natural/BigN/Nbasic.vo
-lib/coq/theories/Numbers/Natural/Binary/NBinDefs.vo
 lib/coq/theories/Numbers/Natural/Binary/NBinary.vo
 lib/coq/theories/Numbers/Natural/Peano/NPeano.vo
 lib/coq/theories/Numbers/Natural/SpecViaZ/NSig.vo
@@ -562,9 +722,11 @@ lib/coq/theories/Program/Utils.vo
 lib/coq/theories/Program/Wf.vo
 lib/coq/theories/QArith/QArith.vo
 lib/coq/theories/QArith/QArith_base.vo
+lib/coq/theories/QArith/QOrderedType.vo
 lib/coq/theories/QArith/Qabs.vo
 lib/coq/theories/QArith/Qcanon.vo
 lib/coq/theories/QArith/Qfield.vo
+lib/coq/theories/QArith/Qminmax.vo
 lib/coq/theories/QArith/Qpower.vo
 lib/coq/theories/QArith/Qreals.vo
 lib/coq/theories/QArith/Qreduction.vo
@@ -587,6 +749,7 @@ lib/coq/theories/Reals/PSeries_reg.vo
 lib/coq/theories/Reals/PartSum.vo
 lib/coq/theories/Reals/RIneq.vo
 lib/coq/theories/Reals/RList.vo
+lib/coq/theories/Reals/ROrderedType.vo
 lib/coq/theories/Reals/R_Ifp.vo
 lib/coq/theories/Reals/R_sqr.vo
 lib/coq/theories/Reals/R_sqrt.vo
@@ -608,6 +771,7 @@ lib/coq/theories/Reals/RiemannInt.vo
 lib/coq/theories/Reals/RiemannInt_SF.vo
 lib/coq/theories/Reals/Rlimit.vo
 lib/coq/theories/Reals/Rlogic.vo
+lib/coq/theories/Reals/Rminmax.vo
 lib/coq/theories/Reals/Rpow_def.vo
 lib/coq/theories/Reals/Rpower.vo
 lib/coq/theories/Reals/Rprod.vo
@@ -654,13 +818,30 @@ lib/coq/theories/Sets/Relations_3.vo
 lib/coq/theories/Sets/Relations_3_facts.vo
 lib/coq/theories/Sets/Uniset.vo
 lib/coq/theories/Sorting/Heap.vo
+lib/coq/theories/Sorting/Mergesort.vo
 lib/coq/theories/Sorting/PermutEq.vo
 lib/coq/theories/Sorting/PermutSetoid.vo
 lib/coq/theories/Sorting/Permutation.vo
+lib/coq/theories/Sorting/Sorted.vo
 lib/coq/theories/Sorting/Sorting.vo
 lib/coq/theories/Strings/Ascii.vo
 lib/coq/theories/Strings/String.vo
+lib/coq/theories/Structures/DecidableType.vo
+lib/coq/theories/Structures/DecidableTypeEx.vo
+lib/coq/theories/Structures/Equalities.vo
+lib/coq/theories/Structures/EqualitiesFacts.vo
+lib/coq/theories/Structures/GenericMinMax.vo
+lib/coq/theories/Structures/OrderedType.vo
+lib/coq/theories/Structures/OrderedTypeAlt.vo
+lib/coq/theories/Structures/OrderedTypeEx.vo
+lib/coq/theories/Structures/Orders.vo
+lib/coq/theories/Structures/OrdersAlt.vo
+lib/coq/theories/Structures/OrdersEx.vo
+lib/coq/theories/Structures/OrdersFacts.vo
+lib/coq/theories/Structures/OrdersLists.vo
+lib/coq/theories/Structures/OrdersTac.vo
 lib/coq/theories/Unicode/Utf8.vo
+lib/coq/theories/Unicode/Utf8_core.vo
 lib/coq/theories/Wellfounded/Disjoint_Union.vo
 lib/coq/theories/Wellfounded/Inclusion.vo
 lib/coq/theories/Wellfounded/Inverse_Image.vo
@@ -678,11 +859,12 @@ lib/coq/theories/ZArith/ZArith_base.vo
 lib/coq/theories/ZArith/ZArith_dec.vo
 lib/coq/theories/ZArith/ZOdiv.vo
 lib/coq/theories/ZArith/ZOdiv_def.vo
+lib/coq/theories/ZArith/ZOrderedType.vo
 lib/coq/theories/ZArith/Zabs.vo
-lib/coq/theories/ZArith/Zbinary.vo
 lib/coq/theories/ZArith/Zbool.vo
 lib/coq/theories/ZArith/Zcompare.vo
 lib/coq/theories/ZArith/Zcomplements.vo
+lib/coq/theories/ZArith/Zdigits.vo
 lib/coq/theories/ZArith/Zdiv.vo
 lib/coq/theories/ZArith/Zeven.vo
 lib/coq/theories/ZArith/Zgcd_alt.vo
@@ -704,6 +886,7 @@ lib/coq/theories/ZArith/auxiliary.vo
 lib/coq/tools/coqdoc/coqdoc.css
 lib/coq/tools/coqdoc/coqdoc.sty
 lib/coq/toplevel/auto_ind_decl.cmi
+lib/coq/toplevel/autoinstance.cmi
 lib/coq/toplevel/cerrors.cmi
 lib/coq/toplevel/class.cmi
 lib/coq/toplevel/classes.cmi
@@ -713,11 +896,13 @@ lib/coq/toplevel/coqtop.cmi
 lib/coq/toplevel/discharge.cmi
 lib/coq/toplevel/himsg.cmi
 lib/coq/toplevel/ind_tables.cmi
-lib/coq/toplevel/line_oriented_parser.cmi
+lib/coq/toplevel/indschemes.cmi
+lib/coq/toplevel/lemmas.cmi
+lib/coq/toplevel/libtypes.cmi
 lib/coq/toplevel/metasyntax.cmi
 lib/coq/toplevel/mltop.cmi
-lib/coq/toplevel/protectedtoplevel.cmi
 lib/coq/toplevel/record.cmi
+lib/coq/toplevel/search.cmi
 lib/coq/toplevel/toplevel.a
 lib/coq/toplevel/toplevel.cma
 lib/coq/toplevel/toplevel.cmi
@@ -728,11 +913,10 @@ lib/coq/toplevel/vernacentries.cmi
 lib/coq/toplevel/vernacexpr.cmi
 lib/coq/toplevel/vernacinterp.cmi
 lib/coq/toplevel/whelp.cmi
-man/man1/coq-interface.1
-man/man1/coq-parser.1
 man/man1/coq-tex.1
 man/man1/coq_makefile.1
 man/man1/coqc.1
+man/man1/coqchk.1
 man/man1/coqdep.1
 man/man1/coqdoc.1
 man/man1/coqide.1
@@ -741,7 +925,10 @@ man/man1/coqtop.1
 man/man1/coqtop.byte.1
 man/man1/coqwc.1
 man/man1/gallina.1
+share/emacs/site-lisp/coq-db.el
+share/emacs/site-lisp/coq-font-lock.el
 share/emacs/site-lisp/coq-inferior.el
+share/emacs/site-lisp/coq-syntax.el
 share/emacs/site-lisp/coq.el
 share/emacs/site-lisp/coqdoc.sty
 @pkgdir lib/coq/user-contrib
diff --git a/lang/coq/PLIST.natdynlink b/lang/coq/PLIST.natdynlink
new file mode 100644
index 00000000000..0570962c264
--- /dev/null
+++ b/lang/coq/PLIST.natdynlink
@@ -0,0 +1,24 @@
+@comment $NetBSD: PLIST.natdynlink,v 1.1 2010/11/14 20:53:02 tonio Exp $
+lib/coq/plugins/cc/cc_plugin.cmxs
+lib/coq/plugins/dp/dp_plugin.cmxs
+lib/coq/plugins/extraction/extraction_plugin.cmxs
+lib/coq/plugins/field/field_plugin.cmxs
+lib/coq/plugins/firstorder/ground_plugin.cmxs
+lib/coq/plugins/fourier/fourier_plugin.cmxs
+lib/coq/plugins/funind/recdef_plugin.cmxs
+lib/coq/plugins/micromega/micromega_plugin.cmxs
+lib/coq/plugins/nsatz/nsatz_plugin.cmxs
+lib/coq/plugins/omega/omega_plugin.cmxs
+lib/coq/plugins/quote/quote_plugin.cmxs
+lib/coq/plugins/ring/ring_plugin.cmxs
+lib/coq/plugins/romega/romega_plugin.cmxs
+lib/coq/plugins/rtauto/rtauto_plugin.cmxs
+lib/coq/plugins/setoid_ring/newring_plugin.cmxs
+lib/coq/plugins/subtac/subtac_plugin.cmxs
+lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
+lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
+lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
+lib/coq/plugins/syntax/r_syntax_plugin.cmxs
+lib/coq/plugins/syntax/string_syntax_plugin.cmxs
+lib/coq/plugins/syntax/z_syntax_plugin.cmxs
+lib/coq/plugins/xml/xml_plugin.cmxs
diff --git a/lang/coq/PLIST.opt b/lang/coq/PLIST.opt
index d650b8b8f3f..1bf1c7da7cb 100644
--- a/lang/coq/PLIST.opt
+++ b/lang/coq/PLIST.opt
@@ -1,6 +1,4 @@
-@comment $NetBSD: PLIST.opt,v 1.6 2009/09/05 20:44:57 tonio Exp $
-bin/coq-interface.opt
-bin/coq-parser.opt
+@comment $NetBSD: PLIST.opt,v 1.7 2010/11/14 20:53:02 tonio Exp $
 bin/coqchk.opt
 ${PLIST.coqide}bin/coqide.opt
 bin/coqtop.opt
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 45585806182..85aff64b172 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,9 +1,8 @@
-$NetBSD: distinfo,v 1.11 2010/11/07 15:39:55 tonio Exp $
+$NetBSD: distinfo,v 1.12 2010/11/14 20:53:02 tonio Exp $
 
-SHA1 (coq-8.2pl1.tar.gz) = 4aed3302adc2edbaa5d97984512c1c13014bd649
-RMD160 (coq-8.2pl1.tar.gz) = dd5758a94bb3de49967cec76baa33eb5169659ce
-Size (coq-8.2pl1.tar.gz) = 3600620 bytes
-SHA1 (patch-aa) = 2725d9fb667f6a66bf9cb6dd0bdcdbd94d8c1fd6
-SHA1 (patch-ab) = 207d8138baf9bfbb78d816c24dcc367869a60569
-SHA1 (patch-ac) = 30780c9f96ad16c814a5edc50bd1edbd030aa9b5
-SHA1 (patch-ad) = 9bb28ca4eeb77d53d3665fbc4575bea1f57c738c
+SHA1 (coq-8.3.tar.gz) = 6c6472b6a41429e78d979eacd8ff58bd6f6c9da4
+RMD160 (coq-8.3.tar.gz) = 9e42266001c0a22b39662be86960a05e454fc2fb
+Size (coq-8.3.tar.gz) = 3736420 bytes
+SHA1 (patch-aa) = 851efa1859b4d8dc7bad549792a5966b549f868e
+SHA1 (patch-ab) = f20f78c936e18ca195933375f37fc5b816827604
+SHA1 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f
diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa
index 026e33168dd..db825e53d81 100644
--- a/lang/coq/patches/patch-aa
+++ b/lang/coq/patches/patch-aa
@@ -1,13 +1,31 @@
-$NetBSD: patch-aa,v 1.8 2009/09/05 20:44:58 tonio Exp $
+$NetBSD: patch-aa,v 1.9 2010/11/14 20:53:03 tonio Exp $
 
---- Makefile.orig	2009-04-08 17:38:39.000000000 +0200
+Fix mixed implicit and normal rules
+This fixes build with GNU Make 3.82. See threads:
+  https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
+  http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
+
+Patch from https://gforge.inria.fr/scm/viewvc.php?diff_format=s&view=rev&root=coq&sortby=file&revision=13566
+
+--- Makefile.orig	2010-10-13 19:53:28.000000000 +0000
 +++ Makefile
-@@ -24,8 +24,6 @@
- # by Emacs' next-error.
- ###########################################################################
+@@ -160,9 +160,19 @@ else
+ stage1 $(STAGE1_TARGETS) : always
+ 	$(call stage-template,1)
+ 
++ifneq (,$(STAGE1_IMPLICITS))
++$(STAGE1_IMPLICITS) : always
++	$(call stage-template,1)
++endif
++
+ stage2 $(STAGE2_TARGETS) : stage1
+ 	$(call stage-template,2)
  
--export SHELL:=/bin/bash
--
- export FIND_VCS_CLAUSE:='(' \
-   -name '{arch}' -o \
-   -name '.svn' -o \
++ifneq (,$(STAGE2_IMPLICITS))
++$(STAGE2_IMPLICITS) : stage1
++	$(call stage-template,2)
++endif
++
+ # Nota:
+ # - world is one of the targets in $(STAGE2_TARGETS), hence launching
+ # "make" or "make world" leads to recursion into stage1 then stage2
diff --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab
index 3f181430a76..7fdf8549107 100644
--- a/lang/coq/patches/patch-ab
+++ b/lang/coq/patches/patch-ab
@@ -1,36 +1,52 @@
-$NetBSD: patch-ab,v 1.3 2010/11/07 15:39:55 tonio Exp $
+$NetBSD: patch-ab,v 1.4 2010/11/14 20:53:03 tonio Exp $
 
---- configure.orig	2009-07-01 09:58:00.000000000 +0000
-+++ configure
-@@ -1,4 +1,4 @@
--#!/bin/bash
-+#!/bin/sh
- 
- ##################################
- #
-@@ -325,13 +325,15 @@ MAKE=`which make`
- if [ "$MAKE" != "" ]; then
-   MAKEVERSION=`$MAKE -v | head -1`
-   case $MAKEVERSION in
-+    "GNU Make 3.82") 
-+      echo "You have GNU Make 3.82. Good!";;
-     "GNU Make 3.81") 
-       echo "You have GNU Make 3.81. Good!";;
-     *)
-       OK="no"
-       if [ -x ./make ]; then
- 	  MAKEVERSION=`./make -v | head -1`
--	  if [ "$MAKEVERSION" == "GNU Make 3.81" ]; then OK="yes"; fi
-+	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
-       fi
-       if [ $OK = "no" ]; then
- 	  echo "GNU Make >= 3.81 is needed"
-@@ -412,7 +414,7 @@ esac
- 
- # this fixes a camlp4 bug under FreeBSD
- # ("native-code program cannot do a dynamic load")
--if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
-+#if [ `uname -s` = "FreeBSD" ]; then camlp4oexec=$camlp4oexec.byte; fi
- 
- CAMLVERSION=`"$bytecamlc" -version`
+Fix mixed implicit and normal rules
+This fixes build with GNU Make 3.82. See threads:
+  https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html
+  http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912
+
+Patch from https://gforge.inria.fr/scm/viewvc.php?diff_format=s&view=rev&root=coq&sortby=file&revision=13566
+
+--- Makefile.common.orig	2010-06-23 13:17:17.000000000 +0000
++++ Makefile.common
+@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y")
+ 
+ SOURCEDOCDIR=dev/source-doc
+ 
+-CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
++CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
+ 
+ ### Targets forwarded by Makefile to a specific stage:
+ 
+@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi 
+ STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
+   $(GENFILES) \
+   source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
+-  $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
++  $(STAGE1_ML4:.ml4=.ml4-preprocessed)
++
++STAGE1_IMPLICITS:=
+ 
+ ifdef CM_STAGE1
+- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
++ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
+ endif
+ 
+ ## Enumeration of targets that require being done at stage2
+@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kerne
+   printers debug initplugins plugins \
+   world install coqide coqide-files coq coqlib \
+   coqlight states check init theories theories-light \
+-  $(DOC_TARGETS) $(VO_TARGETS) validate \
+-  %.vo %.glob states/% install-% %.ml4-preprocessed \
++  $(DOC_TARGETS) $(VO_TARGETS) validate
++
++STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
+   $(DOC_TARGET_PATTERNS)
+ 
+ ifndef CM_STAGE1
+- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
++ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
+ endif
+ 
  
diff --git a/lang/coq/patches/patch-ac b/lang/coq/patches/patch-ac
index 1ac85f2dfb2..f33d8166d96 100644
--- a/lang/coq/patches/patch-ac
+++ b/lang/coq/patches/patch-ac
@@ -1,12 +1,15 @@
-$NetBSD: patch-ac,v 1.1 2009/09/05 20:44:58 tonio Exp $
+$NetBSD: patch-ac,v 1.2 2010/11/14 20:53:03 tonio Exp $
 
---- Makefile.stage1.orig	2009-04-08 17:38:39.000000000 +0200
-+++ Makefile.stage1
-@@ -6,7 +6,6 @@
- #         #       GNU Lesser General Public License Version 2.1       #
- #######################################################################
- 
--export SHELL:=/bin/bash
- include Makefile.build
- 
- # All includes must be declared secondary, otherwise make will delete
+Always install plugins static opt files
+
+--- Makefile.build.orig	2010-09-30 16:50:00.000000000 +0000
++++ Makefile.build
+@@ -592,7 +592,7 @@ install-library:
+           `cat $(CORECMA:.cma=.mllib.d) $(PLUGINSCMA:.cma=.mllib.d) | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.cmi/p"`
+ ifeq ($(BEST),opt)
+ 	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
+-	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
++	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT:.cmxs=.cmxa) $(PLUGINSOPT:.cmxs=.a)
+ endif
+ # csdpcert is not meant to be directly called by the user; we install
+ # it with libraries
diff --git a/lang/coq/patches/patch-ad b/lang/coq/patches/patch-ad
deleted file mode 100644
index 838cc986b91..00000000000
--- a/lang/coq/patches/patch-ad
+++ /dev/null
@@ -1,177 +0,0 @@
-$NetBSD: patch-ad,v 1.1 2009/12/12 21:12:43 asau Exp $
-
---- Makefile.build.orig	2009-06-07 01:43:23.000000000 +0400
-+++ Makefile.build	2009-12-12 23:34:42.000000000 +0300
-@@ -435,22 +435,22 @@
- install-ide-no:
- 
- install-ide-byte: 
--	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQIDEBYTE) $(FULLBINDIR)
--	cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
-+	$(INSTALLBIN) $(COQIDEBYTE) $(DESTDIR)$(FULLBINDIR)
-+	cd $(DESTDIR)$(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
- 
- install-ide-opt:
--	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
--	cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
-+	$(INSTALLBIN) $(COQIDEBYTE) $(COQIDEOPT) $(DESTDIR)$(FULLBINDIR)
-+	cd $(DESTDIR)$(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
- 
- install-ide-files:
--	$(MKDIR) $(FULLIDELIB)
--	$(INSTALLLIB) $(IDEFILES) $(FULLIDELIB)
-+	$(MKDIR) $(DESTDIR)$(FULLIDELIB)
-+	$(INSTALLLIB) $(IDEFILES) $(DESTDIR)$(FULLIDELIB)
- 
- install-ide-info:
--	$(MKDIR) $(FULLIDELIB)
--	$(INSTALLLIB) ide/FAQ $(FULLIDELIB)
-+	$(MKDIR) $(DESTDIR)$(FULLIDELIB)
-+	$(INSTALLLIB) ide/FAQ $(DESTDIR)$(FULLIDELIB)
- 
- ###########################################################################
- # Pcoq: special binaries for debugging (coq-interface, coq-parser)
-@@ -486,16 +486,16 @@
- install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
- 
- install-pcoq-binaries::
--	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQINTERFACE) $(FULLBINDIR)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
-+	$(INSTALLBIN) $(COQINTERFACE) $(DESTDIR)$(FULLBINDIR)
- 
- install-pcoq-files::
--	$(MKDIR) $(FULLCOQLIB)/contrib/interface
--	$(INSTALLLIB) $(INTERFACERC) $(FULLCOQLIB)/contrib/interface
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/contrib/interface
-+	$(INSTALLLIB) $(INTERFACERC) $(DESTDIR)$(FULLCOQLIB)/contrib/interface
- 
- install-pcoq-manpages:
--	$(MKDIR) $(FULLMANDIR)/man1
--	$(INSTALLLIB) $(PCOQMANPAGES) $(FULLMANDIR)/man1
-+	$(MKDIR) $(DESTDIR)$(FULLMANDIR)/man1
-+	$(INSTALLLIB) $(PCOQMANPAGES) $(DESTDIR)$(FULLMANDIR)/man1
- 
- ###########################################################################
- # tests
-@@ -682,77 +682,77 @@
- install-binaries:: install-$(BEST) install-tools
- 
- install-byte::
--	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
--	cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
-+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(DESTDIR)$(FULLBINDIR)
-+	cd $(DESTDIR)$(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
- 
- install-opt::
--	$(MKDIR) $(FULLBINDIR)
--	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
--	cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
-+	$(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(DESTDIR)$(FULLBINDIR)
-+	cd $(DESTDIR)$(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
- 
- install-tools::
--	$(MKDIR) $(FULLBINDIR)
-+	$(MKDIR) $(DESTDIR)$(FULLBINDIR)
- 	# recopie des fichiers de style pour coqide
--	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
--	touch $(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
--	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
--	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/tools/coqdoc
-+	touch $(DESTDIR)$(FULLCOQLIB)/tools/coqdoc/coqdoc.sty $(DESTDIR)$(FULLCOQLIB)/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
-+	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(DESTDIR)$(FULLCOQLIB)/tools/coqdoc
-+	$(INSTALLBIN) $(TOOLS) $(DESTDIR)$(FULLBINDIR)
- 
- install-library:
--	$(MKDIR) $(FULLCOQLIB)
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)
- 	for f in $(LIBFILES); do \
--	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
--	  $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
-+	  $(MKDIR) $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-+	  $(INSTALLLIB) $$f $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-         done
--	$(MKDIR) $(FULLCOQLIB)/states
--	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
--	$(MKDIR) $(FULLCOQLIB)/user-contrib
--	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
--	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA)
--	$(INSTALLSH)  $(FULLCOQLIB) $(OBJSCMO:.cmo=.cmi)
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/states
-+	$(INSTALLLIB) states/*.coq $(DESTDIR)$(FULLCOQLIB)/states
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/user-contrib
-+	$(INSTALLLIB) $(DLLCOQRUN) $(DESTDIR)$(FULLCOQLIB)
-+	$(INSTALLSH)  $(DESTDIR)$(FULLCOQLIB) $(CONFIG) $(LINKCMO) $(GRAMMARCMA)
-+	$(INSTALLSH)  $(DESTDIR)$(FULLCOQLIB) $(OBJSCMO:.cmo=.cmi)
- ifeq ($(BEST),opt)
--	$(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
--	$(INSTALLSH)  $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
-+	$(INSTALLLIB) $(LIBCOQRUN) $(DESTDIR)$(FULLCOQLIB)
-+	$(INSTALLSH)  $(DESTDIR)$(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a)
- endif
- # csdpcert is not meant to be directly called by the user; we install
- # it with libraries
--	-$(MKDIR) $(FULLCOQLIB)/contrib/micromega
--	$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
--	-$(INSTALLLIB) revision $(FULLCOQLIB)
-+	-$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/contrib/micromega
-+	$(INSTALLBIN) $(CSDPCERT) $(DESTDIR)$(FULLCOQLIB)/contrib/micromega
-+	-$(INSTALLLIB) revision $(DESTDIR)$(FULLCOQLIB)
- 
- install-library-light:
--	$(MKDIR) $(FULLCOQLIB)
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)
- 	for f in $(LIBFILESLIGHT); do \
--	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
--	  $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
-+	  $(MKDIR) $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-+	  $(INSTALLLIB) $$f $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-         done
--	$(MKDIR) $(FULLCOQLIB)/states
--	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
--	-$(INSTALLLIB) revision $(FULLCOQLIB)
-+	$(MKDIR) $(DESTDIR)$(FULLCOQLIB)/states
-+	$(INSTALLLIB) states/*.coq $(DESTDIR)$(FULLCOQLIB)/states
-+	-$(INSTALLLIB) revision $(DESTDIR)$(FULLCOQLIB)
- 
- install-allreals::
- 	for f in $(ALLREALS); do \
--	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
--	  $(INSTALLLIB) $$f $(FULLCOQLIB)/`dirname $$f`; \
-+	  $(MKDIR) $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-+	  $(INSTALLLIB) $$f $(DESTDIR)$(FULLCOQLIB)/`dirname $$f`; \
-         done
- 
- install-coq-info: install-coq-manpages install-emacs install-latex
- 
- install-coq-manpages:
--	$(MKDIR) $(FULLMANDIR)/man1
--	$(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1
-+	$(MKDIR) $(DESTDIR)$(FULLMANDIR)/man1
-+	$(INSTALLLIB) $(MANPAGES) $(DESTDIR)$(FULLMANDIR)/man1
- 
- install-emacs:
--	$(MKDIR) $(FULLEMACSLIB)
--	$(INSTALLLIB) tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
-+	$(MKDIR) $(DESTDIR)$(FULLEMACSLIB)
-+	$(INSTALLLIB) tools/coq.el tools/coq-inferior.el $(DESTDIR)$(FULLEMACSLIB)
- 
- # command to update TeX' kpathsea database
- #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
- 
- install-latex:
--	$(MKDIR) $(FULLCOQDOCDIR)
--	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
-+	$(MKDIR) $(DESTDIR)$(FULLCOQDOCDIR)
-+	$(INSTALLLIB) tools/coqdoc/coqdoc.sty $(DESTDIR)$(FULLCOQDOCDIR)	
- #	-$(UPDATETEX)
- 
- ###########################################################################