summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lang/coq/Makefile30
-rw-r--r--lang/coq/PLIST174
-rw-r--r--lang/coq/PLIST.natdynlink24
-rw-r--r--lang/coq/PLIST.opt5
-rw-r--r--lang/coq/distinfo12
-rw-r--r--lang/coq/patches/patch-Makefile.build32
-rw-r--r--lang/coq/patches/patch-ac15
-rw-r--r--lang/coq/patches/patch-ide_preferences.ml16
-rw-r--r--lang/coq/patches/patch-ide_utils_okey.ml29
9 files changed, 236 insertions, 101 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index df18b0a9547..903d342ae8b 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,12 +1,11 @@
-# $NetBSD: Makefile,v 1.50 2012/10/08 23:01:57 adam Exp $
+# $NetBSD: Makefile,v 1.51 2012/10/29 11:33:17 jaapb Exp $
#
-DISTNAME= coq-8.3pl1
-PKGREVISION= 16
+DISTNAME= coq-8.4
CATEGORIES= lang math
-MASTER_SITES= http://coq.inria.fr/distrib/V8.3pl1/files/
+MASTER_SITES= http://coq.inria.fr/distrib/V8.4/files/
-MAINTAINER= richards+netbsd@CS.Princeton.EDU
+MAINTAINER= jaapb@NetBSD.org
HOMEPAGE= http://coq.inria.fr/
COMMENT= Theorem prover which extracts programs from proofs
LICENSE= gnu-lgpl-v2.1
@@ -15,6 +14,8 @@ USE_TOOLS+= gmake
HAS_CONFIGURE= YES
CONFIGURE_ARGS+= -prefix ${PREFIX}
CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp
+CONFIGURE_ARGS+= -mandir ${PREFIX}/${PKGMANDIR}
+CONFIGURE_ARGS+= -configdir ${PKG_SYSCONFDIR}/xdg/coq
BUILD_TARGET= world
BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
@@ -22,8 +23,13 @@ BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10
.include "../../mk/bsd.prefs.mk"
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \
- (${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64")
-PLIST_SRC= ${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
+ (${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64") || \
+ (${MACHINE_ARCH} == "arm")
+PLIST.opt= yes
+COQIDE_TYPE= opt
+.else
+PLIST.byte= yes
+COQIDE_TYPE= byte
.endif
.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
@@ -31,7 +37,7 @@ PLIST_SRC= ${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
!empty(MACHINE_PLATFORM:MDragonFly-*-*) || \
!empty(MACHINE_PLATFORM:MFreeBSD-*-*) || \
!empty(MACHINE_PLATFORM:MNetBSD-*-*)
-PLIST_SRC+= ${PKGDIR}/PLIST.natdynlink
+PLIST.natdynlink= yes
. endif
.endif
@@ -46,7 +52,7 @@ _STRIPFLAG_INSTALL=
REPLACE_SH= configure install.sh
INSTALL_ENV+= COQINSTALLPREFIX=${DESTDIR}
-PLIST_VARS= coqide
+PLIST_VARS= coqide byte opt natdynlink
PKG_OPTIONS_VAR= PKG_OPTIONS.coq
PKG_SUPPORTED_OPTIONS= coqide
.include "../../mk/bsd.options.mk"
@@ -54,8 +60,14 @@ PKG_SUPPORTED_OPTIONS= coqide
.include "../../x11/lablgtk/buildlink3.mk"
.include "../../x11/gtk2/buildlink3.mk"
PLIST.coqide= yes
+CONFIGURE_ARGS+= -coqide ${COQIDE_TYPE}
+.else
+CONFIGURE_ARGS+= -coqide no
.endif
+EGDIR= ${PREFIX}/share/coq/examples
+CONF_FILES= ${EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc
+
.include "../../mk/pthread.buildlink3.mk"
.include "../../lang/ocaml/buildlink3.mk"
.include "../../lang/camlp5/buildlink3.mk"
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index 253cace0ed9..befc95ce398 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,15 +1,18 @@
-@comment $NetBSD: PLIST,v 1.11 2010/11/14 20:53:02 tonio Exp $
+@comment $NetBSD: PLIST,v 1.12 2012/10/29 11:33:17 jaapb Exp $
bin/coq-tex
bin/coq_makefile
bin/coqc
bin/coqchk
+${PLIST.opt}bin/coqchk.opt
bin/coqdep
bin/coqdoc
${PLIST.coqide}bin/coqide
+${PLIST.coqide}${PLIST.byte}bin/coqide.byte
+${PLIST.coqide}${PLIST.opt}bin/coqide.opt
bin/coqmktop
bin/coqtop
bin/coqtop.byte
-${PLIST.coqide}bin/coqide.byte
+${PLIST.opt}bin/coqtop.opt
bin/coqwc
bin/gallina
lib/coq/config/coq_config.cmi
@@ -17,23 +20,22 @@ lib/coq/config/coq_config.cmo
lib/coq/config/coq_config.cmx
lib/coq/config/coq_config.o
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/coqide_ui.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/ideproof.cmi
${PLIST.coqide}lib/coq/ide/ideutils.cmi
+${PLIST.coqide}lib/coq/ide/minilib.cmi
${PLIST.coqide}lib/coq/ide/preferences.cmi
+${PLIST.coqide}lib/coq/ide/project_file.cmi
${PLIST.coqide}lib/coq/ide/tags.cmi
${PLIST.coqide}lib/coq/ide/typed_notebook.cmi
${PLIST.coqide}lib/coq/ide/undo.cmi
@@ -97,20 +99,19 @@ lib/coq/kernel/univ.cmi
lib/coq/kernel/vconv.cmi
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/errors.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
lib/coq/lib/hashcons.cmi
+lib/coq/lib/hashtbl_alt.cmi
lib/coq/lib/heap.cmi
lib/coq/lib/lib.a
lib/coq/lib/lib.cma
@@ -122,12 +123,17 @@ lib/coq/lib/predicate.cmi
lib/coq/lib/profile.cmi
lib/coq/lib/rtree.cmi
lib/coq/lib/segmenttree.cmi
+lib/coq/lib/store.cmi
lib/coq/lib/system.cmi
-lib/coq/lib/tlm.cmi
lib/coq/lib/tries.cmi
lib/coq/lib/unicodetable.cmi
+lib/coq/lib/unionfind.cmi
lib/coq/lib/util.cmi
+lib/coq/lib/xml_lexer.cmi
+lib/coq/lib/xml_parser.cmi
+lib/coq/lib/xml_utils.cmi
lib/coq/libcoqrun.a
+lib/coq/library/assumptions.cmi
lib/coq/library/decl_kinds.cmi
lib/coq/library/declare.cmi
lib/coq/library/declaremods.cmi
@@ -135,6 +141,7 @@ lib/coq/library/decls.cmi
lib/coq/library/dischargedhypsmap.cmi
lib/coq/library/global.cmi
lib/coq/library/goptions.cmi
+lib/coq/library/goptionstyp.cmi
lib/coq/library/heads.cmi
lib/coq/library/impargs.cmi
lib/coq/library/lib.cmi
@@ -152,7 +159,6 @@ lib/coq/parsing/egrammar.cmi
lib/coq/parsing/extend.cmi
lib/coq/parsing/extrawit.cmi
lib/coq/parsing/g_constr.cmi
-lib/coq/parsing/g_decl_mode.cmi
lib/coq/parsing/g_ltac.cmi
lib/coq/parsing/g_prim.cmi
lib/coq/parsing/g_proofs.cmi
@@ -169,30 +175,34 @@ lib/coq/parsing/parsing.cma
lib/coq/parsing/parsing.cmxa
lib/coq/parsing/pcoq.cmi
lib/coq/parsing/ppconstr.cmi
-lib/coq/parsing/ppdecl_proof.cmi
lib/coq/parsing/pptactic.cmi
lib/coq/parsing/ppvernac.cmi
lib/coq/parsing/prettyp.cmi
lib/coq/parsing/printer.cmi
lib/coq/parsing/printmod.cmi
+lib/coq/parsing/q_util.cmi
lib/coq/parsing/tactic_printer.cmi
+lib/coq/parsing/tok.cmi
lib/coq/plugins/cc/cc_plugin.a
lib/coq/plugins/cc/cc_plugin.cma
-lib/coq/plugins/cc/cc_plugin.cmxa
+${PLIST.opt}lib/coq/plugins/cc/cc_plugin.cmxa
+${PLIST.natdynlink}lib/coq/plugins/cc/cc_plugin.cmxs
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/decl_mode/decl_expr.cmi
+lib/coq/plugins/decl_mode/decl_interp.cmi
+lib/coq/plugins/decl_mode/decl_mode.cmi
+lib/coq/plugins/decl_mode/decl_mode_plugin.a
+lib/coq/plugins/decl_mode/decl_mode_plugin.cma
+${PLIST.opt}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxa
+${PLIST.natdynlink}lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
+lib/coq/plugins/decl_mode/decl_mode_plugin_mod.cmi
+lib/coq/plugins/decl_mode/decl_proof_instr.cmi
+lib/coq/plugins/decl_mode/g_decl_mode.cmi
+lib/coq/plugins/decl_mode/ppdecl_proof.cmi
lib/coq/plugins/extraction/ExtrOcamlBasic.vo
lib/coq/plugins/extraction/ExtrOcamlBigIntConv.vo
lib/coq/plugins/extraction/ExtrOcamlIntConv.vo
@@ -207,9 +217,11 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/extraction/extraction_plugin.cmxs
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/miniml.cmi
lib/coq/plugins/extraction/mlutil.cmi
lib/coq/plugins/extraction/modutil.cmi
lib/coq/plugins/extraction/ocaml.cmi
@@ -223,6 +235,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/field/field_plugin.cmxs
lib/coq/plugins/field/field_plugin_mod.cmi
lib/coq/plugins/firstorder/formula.cmi
lib/coq/plugins/firstorder/g_ground.cmi
@@ -230,6 +243,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/firstorder/ground_plugin.cmxs
lib/coq/plugins/firstorder/ground_plugin_mod.cmi
lib/coq/plugins/firstorder/instances.cmi
lib/coq/plugins/firstorder/rules.cmi
@@ -242,22 +256,24 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/fourier/fourier_plugin.cmxs
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/glob_term_to_relation.cmi
+lib/coq/plugins/funind/glob_termops.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
+${PLIST.natdynlink}lib/coq/plugins/funind/recdef_plugin.cmxs
lib/coq/plugins/funind/recdef_plugin_mod.cmi
lib/coq/plugins/micromega/CheckerMaker.vo
lib/coq/plugins/micromega/Env.vo
@@ -281,9 +297,12 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/micromega/micromega_plugin.cmxs
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/polynomial.cmi
+lib/coq/plugins/micromega/sos.cmi
lib/coq/plugins/micromega/sos_types.cmi
lib/coq/plugins/nsatz/Nsatz.vo
lib/coq/plugins/nsatz/ideal.cmi
@@ -291,6 +310,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/nsatz/nsatz_plugin.cmxs
lib/coq/plugins/nsatz/nsatz_plugin_mod.cmi
lib/coq/plugins/nsatz/polynom.cmi
lib/coq/plugins/nsatz/utile.cmi
@@ -304,6 +324,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/omega/omega_plugin.cmxs
lib/coq/plugins/omega/omega_plugin_mod.cmi
lib/coq/plugins/quote/Quote.vo
lib/coq/plugins/quote/g_quote.cmi
@@ -311,6 +332,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/quote/quote_plugin.cmxs
lib/coq/plugins/quote/quote_plugin_mod.cmi
lib/coq/plugins/ring/LegacyArithRing.vo
lib/coq/plugins/ring/LegacyNArithRing.vo
@@ -327,6 +349,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/ring/ring_plugin.cmxs
lib/coq/plugins/ring/ring_plugin_mod.cmi
lib/coq/plugins/romega/ROmega.vo
lib/coq/plugins/romega/ReflOmegaCore.vo
@@ -336,6 +359,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/romega/romega_plugin.cmxs
lib/coq/plugins/romega/romega_plugin_mod.cmi
lib/coq/plugins/rtauto/Bintree.vo
lib/coq/plugins/rtauto/Rtauto.vo
@@ -345,14 +369,22 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/rtauto/rtauto_plugin.cmxs
lib/coq/plugins/rtauto/rtauto_plugin_mod.cmi
+lib/coq/plugins/setoid_ring/Algebra_syntax.vo
lib/coq/plugins/setoid_ring/ArithRing.vo
lib/coq/plugins/setoid_ring/BinList.vo
+lib/coq/plugins/setoid_ring/Cring.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/Integral_domain.vo
lib/coq/plugins/setoid_ring/NArithRing.vo
+lib/coq/plugins/setoid_ring/Ncring.vo
+lib/coq/plugins/setoid_ring/Ncring_initial.vo
+lib/coq/plugins/setoid_ring/Ncring_polynom.vo
+lib/coq/plugins/setoid_ring/Ncring_tac.vo
lib/coq/plugins/setoid_ring/RealField.vo
lib/coq/plugins/setoid_ring/Ring.vo
lib/coq/plugins/setoid_ring/Ring_base.vo
@@ -360,11 +392,15 @@ 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/Rings_Q.vo
+lib/coq/plugins/setoid_ring/Rings_R.vo
+lib/coq/plugins/setoid_ring/Rings_Z.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
+${PLIST.natdynlink}lib/coq/plugins/setoid_ring/newring_plugin.cmxs
lib/coq/plugins/setoid_ring/newring_plugin_mod.cmi
lib/coq/plugins/subtac/eterm.cmi
lib/coq/plugins/subtac/g_subtac.cmi
@@ -378,6 +414,7 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/subtac/subtac_plugin.cmxs
lib/coq/plugins/subtac/subtac_plugin_mod.cmi
lib/coq/plugins/subtac/subtac_pretyping.cmi
lib/coq/plugins/subtac/subtac_pretyping_F.cmi
@@ -386,31 +423,37 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
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
+${PLIST.natdynlink}lib/coq/plugins/syntax/nat_syntax_plugin.cmxs
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
+${PLIST.natdynlink}lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs
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
+${PLIST.natdynlink}lib/coq/plugins/syntax/r_syntax_plugin.cmxs
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
+${PLIST.natdynlink}lib/coq/plugins/syntax/string_syntax_plugin.cmxs
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
+${PLIST.natdynlink}lib/coq/plugins/syntax/z_syntax_plugin.cmxs
lib/coq/plugins/syntax/z_syntax_plugin_mod.cmi
lib/coq/plugins/xml/acic.cmi
lib/coq/plugins/xml/acic2Xml.cmi
@@ -425,18 +468,20 @@ 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
+${PLIST.natdynlink}lib/coq/plugins/xml/xml_plugin.cmxs
lib/coq/plugins/xml/xml_plugin_mod.cmi
lib/coq/plugins/xml/xmlcommand.cmi
lib/coq/plugins/xml/xmlentries.cmi
+lib/coq/pretyping/arguments_renaming.cmi
lib/coq/pretyping/cases.cmi
lib/coq/pretyping/cbv.cmi
lib/coq/pretyping/classops.cmi
-lib/coq/pretyping/clenv.cmi
lib/coq/pretyping/coercion.cmi
lib/coq/pretyping/detyping.cmi
lib/coq/pretyping/evarconv.cmi
lib/coq/pretyping/evarutil.cmi
lib/coq/pretyping/evd.cmi
+lib/coq/pretyping/glob_term.cmi
lib/coq/pretyping/indrec.cmi
lib/coq/pretyping/inductiveops.cmi
lib/coq/pretyping/matching.cmi
@@ -447,7 +492,6 @@ lib/coq/pretyping/pretyping.a
lib/coq/pretyping/pretyping.cma
lib/coq/pretyping/pretyping.cmi
lib/coq/pretyping/pretyping.cmxa
-lib/coq/pretyping/rawterm.cmi
lib/coq/pretyping/recordops.cmi
lib/coq/pretyping/reductionops.cmi
lib/coq/pretyping/retyping.cmi
@@ -459,16 +503,19 @@ lib/coq/pretyping/typeclasses_errors.cmi
lib/coq/pretyping/typing.cmi
lib/coq/pretyping/unification.cmi
lib/coq/pretyping/vnorm.cmi
+lib/coq/proofs/clenv.cmi
lib/coq/proofs/clenvtac.cmi
-lib/coq/proofs/decl_mode.cmi
lib/coq/proofs/evar_refiner.cmi
+lib/coq/proofs/goal.cmi
lib/coq/proofs/logic.cmi
lib/coq/proofs/pfedit.cmi
-lib/coq/proofs/proof_trees.cmi
+lib/coq/proofs/proof.cmi
+lib/coq/proofs/proof_global.cmi
lib/coq/proofs/proof_type.cmi
lib/coq/proofs/proofs.a
lib/coq/proofs/proofs.cma
lib/coq/proofs/proofs.cmxa
+lib/coq/proofs/proofview.cmi
lib/coq/proofs/redexpr.cmi
lib/coq/proofs/refiner.cmi
lib/coq/proofs/tacexpr.cmi
@@ -480,9 +527,6 @@ lib/coq/tactics/autorewrite.cmi
lib/coq/tactics/btermdn.cmi
lib/coq/tactics/class_tactics.cmi
lib/coq/tactics/contradiction.cmi
-lib/coq/tactics/decl_interp.cmi
-lib/coq/tactics/decl_proof_instr.cmi
-lib/coq/tactics/dhyp.cmi
lib/coq/tactics/dn.cmi
lib/coq/tactics/eauto.cmi
lib/coq/tactics/elim.cmi
@@ -528,10 +572,8 @@ 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
@@ -587,9 +629,9 @@ lib/coq/theories/Lists/List.vo
lib/coq/theories/Lists/ListSet.vo
lib/coq/theories/Lists/ListTactics.vo
lib/coq/theories/Lists/SetoidList.vo
+lib/coq/theories/Lists/SetoidPermutation.vo
lib/coq/theories/Lists/StreamMemo.vo
lib/coq/theories/Lists/Streams.vo
-lib/coq/theories/Lists/TheoryList.vo
lib/coq/theories/Logic/Berardi.vo
lib/coq/theories/Logic/ChoiceFacts.vo
lib/coq/theories/Logic/Classical.vo
@@ -622,25 +664,26 @@ 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/MSetGenTree.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/MSetRBT.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/BinNatDef.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/Ndiv_def.vo
+lib/coq/theories/NArith/Ngcd_def.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/NArith/Nsqrt_def.vo
+lib/coq/theories/Numbers/BinNums.vo
lib/coq/theories/Numbers/BigNumPrelude.vo
lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo
lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo
@@ -662,12 +705,18 @@ 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/ZBits.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/ZGcd.vo
lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZLcm.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZMaxMin.vo
lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo
lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZParity.vo
+lib/coq/theories/Numbers/Integer/Abstract/ZPow.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
@@ -681,22 +730,36 @@ 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/NZBits.vo
lib/coq/theories/Numbers/NatInt/NZDiv.vo
lib/coq/theories/Numbers/NatInt/NZDomain.vo
+lib/coq/theories/Numbers/NatInt/NZGcd.vo
+lib/coq/theories/Numbers/NatInt/NZLog.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/NZParity.vo
+lib/coq/theories/Numbers/NatInt/NZPow.vo
lib/coq/theories/Numbers/NatInt/NZProperties.vo
+lib/coq/theories/Numbers/NatInt/NZSqrt.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/NBits.vo
lib/coq/theories/Numbers/Natural/Abstract/NDefOps.vo
lib/coq/theories/Numbers/Natural/Abstract/NDiv.vo
+lib/coq/theories/Numbers/Natural/Abstract/NGcd.vo
lib/coq/theories/Numbers/Natural/Abstract/NIso.vo
+lib/coq/theories/Numbers/Natural/Abstract/NLcm.vo
+lib/coq/theories/Numbers/Natural/Abstract/NLog.vo
+lib/coq/theories/Numbers/Natural/Abstract/NMaxMin.vo
lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo
lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo
+lib/coq/theories/Numbers/Natural/Abstract/NParity.vo
+lib/coq/theories/Numbers/Natural/Abstract/NPow.vo
lib/coq/theories/Numbers/Natural/Abstract/NProperties.vo
+lib/coq/theories/Numbers/Natural/Abstract/NSqrt.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
@@ -711,6 +774,11 @@ lib/coq/theories/Numbers/NumPrelude.vo
lib/coq/theories/Numbers/Rational/BigQ/BigQ.vo
lib/coq/theories/Numbers/Rational/BigQ/QMake.vo
lib/coq/theories/Numbers/Rational/SpecViaQ/QSig.vo
+lib/coq/theories/PArith/BinPos.vo
+lib/coq/theories/PArith/BinPosDef.vo
+lib/coq/theories/PArith/PArith.vo
+lib/coq/theories/PArith/POrderedType.vo
+lib/coq/theories/PArith/Pnat.vo
lib/coq/theories/Program/Basics.vo
lib/coq/theories/Program/Combinators.vo
lib/coq/theories/Program/Equality.vo
@@ -743,6 +811,7 @@ lib/coq/theories/Reals/DiscrR.vo
lib/coq/theories/Reals/Exp_prop.vo
lib/coq/theories/Reals/Integration.vo
lib/coq/theories/Reals/LegacyRfield.vo
+lib/coq/theories/Reals/Machin.vo
lib/coq/theories/Reals/MVT.vo
lib/coq/theories/Reals/NewtonInt.vo
lib/coq/theories/Reals/PSeries_reg.vo
@@ -758,6 +827,9 @@ lib/coq/theories/Reals/Ranalysis1.vo
lib/coq/theories/Reals/Ranalysis2.vo
lib/coq/theories/Reals/Ranalysis3.vo
lib/coq/theories/Reals/Ranalysis4.vo
+lib/coq/theories/Reals/Ranalysis5.vo
+lib/coq/theories/Reals/Ranalysis_reg.vo
+lib/coq/theories/Reals/Ratan.vo
lib/coq/theories/Reals/Raxioms.vo
lib/coq/theories/Reals/Rbase.vo
lib/coq/theories/Reals/Rbasic_fun.vo
@@ -780,6 +852,7 @@ lib/coq/theories/Reals/Rsigma.vo
lib/coq/theories/Reals/Rsqrt_def.vo
lib/coq/theories/Reals/Rtopology.vo
lib/coq/theories/Reals/Rtrigo.vo
+lib/coq/theories/Reals/Rtrigo1.vo
lib/coq/theories/Reals/Rtrigo_alt.vo
lib/coq/theories/Reals/Rtrigo_calc.vo
lib/coq/theories/Reals/Rtrigo_def.vo
@@ -842,6 +915,10 @@ 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/Vectors/Fin.vo
+lib/coq/theories/Vectors/Vector.vo
+lib/coq/theories/Vectors/VectorDef.vo
+lib/coq/theories/Vectors/VectorSpec.vo
lib/coq/theories/Wellfounded/Disjoint_Union.vo
lib/coq/theories/Wellfounded/Inclusion.vo
lib/coq/theories/Wellfounded/Inverse_Image.vo
@@ -852,6 +929,7 @@ lib/coq/theories/Wellfounded/Union.vo
lib/coq/theories/Wellfounded/Well_Ordering.vo
lib/coq/theories/Wellfounded/Wellfounded.vo
lib/coq/theories/ZArith/BinInt.vo
+lib/coq/theories/ZArith/BinIntDef.vo
lib/coq/theories/ZArith/Int.vo
lib/coq/theories/ZArith/Wf_Z.vo
lib/coq/theories/ZArith/ZArith.vo
@@ -859,13 +937,13 @@ 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/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/Zeuclid.vo
lib/coq/theories/ZArith/Zeven.vo
lib/coq/theories/ZArith/Zgcd_alt.vo
lib/coq/theories/ZArith/Zhints.vo
@@ -877,16 +955,19 @@ lib/coq/theories/ZArith/Zmisc.vo
lib/coq/theories/ZArith/Znat.vo
lib/coq/theories/ZArith/Znumtheory.vo
lib/coq/theories/ZArith/Zorder.vo
+lib/coq/theories/ZArith/Zpow_alt.vo
lib/coq/theories/ZArith/Zpow_def.vo
lib/coq/theories/ZArith/Zpow_facts.vo
lib/coq/theories/ZArith/Zpower.vo
-lib/coq/theories/ZArith/Zsqrt.vo
+lib/coq/theories/ZArith/Zquot.vo
+lib/coq/theories/ZArith/Zsqrt_compat.vo
lib/coq/theories/ZArith/Zwf.vo
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/backtrack.cmi
lib/coq/toplevel/cerrors.cmi
lib/coq/toplevel/class.cmi
lib/coq/toplevel/classes.cmi
@@ -895,8 +976,11 @@ lib/coq/toplevel/coqinit.cmi
lib/coq/toplevel/coqtop.cmi
lib/coq/toplevel/discharge.cmi
lib/coq/toplevel/himsg.cmi
+lib/coq/toplevel/ide_intf.cmi
+lib/coq/toplevel/ide_slave.cmi
lib/coq/toplevel/ind_tables.cmi
lib/coq/toplevel/indschemes.cmi
+lib/coq/toplevel/interface.cmi
lib/coq/toplevel/lemmas.cmi
lib/coq/toplevel/libtypes.cmi
lib/coq/toplevel/metasyntax.cmi
@@ -923,8 +1007,12 @@ man/man1/coqide.1
man/man1/coqmktop.1
man/man1/coqtop.1
man/man1/coqtop.byte.1
+man/man1/coqtop.opt.1
man/man1/coqwc.1
man/man1/gallina.1
+share/coq/coq.png
+share/coq/examples/coqide-gtk2rc
+share/doc/coq/FAQ-CoqIde
share/emacs/site-lisp/coq-db.el
share/emacs/site-lisp/coq-font-lock.el
share/emacs/site-lisp/coq-inferior.el
diff --git a/lang/coq/PLIST.natdynlink b/lang/coq/PLIST.natdynlink
deleted file mode 100644
index 0570962c264..00000000000
--- a/lang/coq/PLIST.natdynlink
+++ /dev/null
@@ -1,24 +0,0 @@
-@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
deleted file mode 100644
index 1bf1c7da7cb..00000000000
--- a/lang/coq/PLIST.opt
+++ /dev/null
@@ -1,5 +0,0 @@
-@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
-man/man1/coqtop.opt.1
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index 8a6e9a540f7..b528bb8eff2 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,6 +1,8 @@
-$NetBSD: distinfo,v 1.13 2011/03/28 20:39:26 tonio Exp $
+$NetBSD: distinfo,v 1.14 2012/10/29 11:33:17 jaapb Exp $
-SHA1 (coq-8.3pl1.tar.gz) = 3fae9fa2fd6f39c9fb3c0b67fcd5e71f1e7a5f9f
-RMD160 (coq-8.3pl1.tar.gz) = 687983bcaca723299b6ea902a1e1b07338209d55
-Size (coq-8.3pl1.tar.gz) = 3756961 bytes
-SHA1 (patch-ac) = 59516eb44aa6cedb4f897b5ac3e8fe0aa69aba0f
+SHA1 (coq-8.4.tar.gz) = 2987aa418dd96a0df7284afe296293cb28814ef5
+RMD160 (coq-8.4.tar.gz) = 6824f9542c823c7d943a59acefb90ff9c9dbe37a
+Size (coq-8.4.tar.gz) = 4134779 bytes
+SHA1 (patch-Makefile.build) = 3fa72d701a80f363ef637e3cbd0e4c2d410da6c4
+SHA1 (patch-ide_preferences.ml) = 625b8e7fe7b4f1612c7f43bd634070aff928fdfb
+SHA1 (patch-ide_utils_okey.ml) = d61ad0e2ea23c531bb4f5e9540f8581a72b54da8
diff --git a/lang/coq/patches/patch-Makefile.build b/lang/coq/patches/patch-Makefile.build
new file mode 100644
index 00000000000..66786e36ef2
--- /dev/null
+++ b/lang/coq/patches/patch-Makefile.build
@@ -0,0 +1,32 @@
+$NetBSD: patch-Makefile.build,v 1.1 2012/10/29 11:33:18 jaapb Exp $
+
+Install configuration file in examples directory
+--- Makefile.build.orig 2012-08-10 21:53:21.000000000 +0000
++++ Makefile.build
+@@ -575,7 +575,7 @@ endif
+ ifdef COQINSTALLPREFIX
+ FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+ FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+-FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
++FULLCONFIGDIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)/examples
+ FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+ FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+ FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%)
+@@ -584,7 +584,7 @@ FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQI
+ else
+ FULLBINDIR=$(BINDIR)
+ FULLCOQLIB=$(COQLIBINSTALL)
+-FULLCONFIGDIR=$(CONFIGDIR)
++FULLCONFIGDIR=$(DATADIR)/examples
+ FULLDATADIR=$(DATADIR)
+ FULLMANDIR=$(MANDIR)
+ FULLEMACSLIB=$(EMACSLIB)
+@@ -638,7 +638,7 @@ install-library:
+ $(INSTALLSH) $(FULLCOQLIB) $(INSTALLCMI)
+ ifeq ($(BEST),opt)
+ $(INSTALLLIB) $(LIBCOQRUN) $(FULLCOQLIB)
+- $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT)
++ $(INSTALLSH) $(FULLCOQLIB) $(CONFIG:.cmo=.cmx) $(CONFIG:.cmo=.o) $(LINKCMO:.cma=.cmxa) $(LINKCMO:.cma=.a) $(PLUGINSOPT) $(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-ac b/lang/coq/patches/patch-ac
deleted file mode 100644
index f33d8166d96..00000000000
--- a/lang/coq/patches/patch-ac
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-ac,v 1.2 2010/11/14 20:53:03 tonio Exp $
-
-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-ide_preferences.ml b/lang/coq/patches/patch-ide_preferences.ml
new file mode 100644
index 00000000000..0c11c0ce910
--- /dev/null
+++ b/lang/coq/patches/patch-ide_preferences.ml
@@ -0,0 +1,16 @@
+$NetBSD: patch-ide_preferences.ml,v 1.1 2012/10/29 11:33:18 jaapb Exp $
+
+Correct for compilation with lablgtk 2.16
+--- ide/preferences.ml.orig 2012-08-08 18:54:37.000000000 +0000
++++ ide/preferences.ml
+@@ -35,6 +35,10 @@ let mod_to_str (m:Gdk.Tags.modifier) =
+ | `MOD5 -> "<Mod5>"
+ | `CONTROL -> "<Control>"
+ | `SHIFT -> "<Shift>"
++ | `HYPER -> "<Hyper>"
++ | `META -> "<Meta>"
++ | `RELEASE -> ""
++ | `SUPER -> "<Super>"
+ | `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
+
+ let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
diff --git a/lang/coq/patches/patch-ide_utils_okey.ml b/lang/coq/patches/patch-ide_utils_okey.ml
new file mode 100644
index 00000000000..8ed5cfd5ef5
--- /dev/null
+++ b/lang/coq/patches/patch-ide_utils_okey.ml
@@ -0,0 +1,29 @@
+$NetBSD: patch-ide_utils_okey.ml,v 1.1 2012/10/29 11:33:18 jaapb Exp $
+
+Correct for compilation with lablgtk 2.16
+--- ide/utils/okey.ml.orig 2006-03-08 11:44:47.000000000 +0000
++++ ide/utils/okey.ml
+@@ -47,6 +47,10 @@ let int_of_modifier = function
+ | `BUTTON3 -> 1024
+ | `BUTTON4 -> 2048
+ | `BUTTON5 -> 4096
++ | `HYPER -> 1 lsl 22
++ | `META -> 1 lsl 20
++ | `RELEASE -> 1 lsl 30
++ | `SUPER -> 1 lsl 21
+
+ let print_modifier l =
+ List.iter
+@@ -65,7 +69,11 @@ let print_modifier l =
+ | `BUTTON2 -> "B2"
+ | `BUTTON3 -> "B3"
+ | `BUTTON4 -> "B4"
+- | `BUTTON5 -> "B5")
++ | `BUTTON5 -> "B5"
++ | `HYPER -> "HYPER"
++ | `META -> "META"
++ | `RELEASE -> ""
++ | `SUPER -> "SUPER")
+ m)^" ")
+ )
+ l;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 07:15:53 +0000