diff options
Diffstat (limited to 'lang/coq')
| -rw-r--r-- | lang/coq/Makefile | 13 | ||||
| -rw-r--r-- | lang/coq/PLIST | 505 | ||||
| -rw-r--r-- | lang/coq/PLIST.opt | 5 | ||||
| -rw-r--r-- | lang/coq/distinfo | 13 | ||||
| -rw-r--r-- | lang/coq/patches/patch-aa | 173 | ||||
| -rw-r--r-- | lang/coq/patches/patch-ab | 17 | ||||
| -rw-r--r-- | lang/coq/patches/patch-ac | 12 |
7 files changed, 498 insertions, 240 deletions
diff --git a/lang/coq/Makefile b/lang/coq/Makefile index 2412f8e2110..14414ea6364 100644 --- a/lang/coq/Makefile +++ b/lang/coq/Makefile @@ -1,10 +1,9 @@ -# $NetBSD: Makefile,v 1.22 2009/08/26 19:57:54 sno Exp $ +# $NetBSD: Makefile,v 1.23 2009/09/05 20:44:57 tonio Exp $ # -DISTNAME= coq-8.1pl3 -PKGREVISION= 2 +DISTNAME= coq-8.2pl1 CATEGORIES= lang math -MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.1pl3/ +MASTER_SITES= http://coq.inria.fr/distrib/V8.2pl1/files/ MAINTAINER= richards+netbsd@CS.Princeton.EDU HOMEPAGE= http://coq.inria.fr/ @@ -17,7 +16,7 @@ CONFIGURE_ARGS+= -emacslib ${PREFIX}/share/emacs/site-lisp CONFIGURE_ARGS+= -reals all BUILD_TARGET= world -BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.09 +BUILDLINK_API_DEPENDS.ocaml+= ocaml>=3.10 .include "../../mk/bsd.prefs.mk" @@ -34,6 +33,10 @@ _STRIPFLAG_CC= _STRIPFLAG_INSTALL= .endif +REPLACE_SH= configure install.sh +CONFIGURE_ENV+= SHELL=${SH:Q} +MAKE_ENV+= SHELL=${SH:Q} + PLIST_VARS= coqide PKG_OPTIONS_VAR= PKG_OPTIONS.coq PKG_SUPPORTED_OPTIONS= coqide diff --git a/lang/coq/PLIST b/lang/coq/PLIST index ceca5865564..7f1dc99f3d8 100644 --- a/lang/coq/PLIST +++ b/lang/coq/PLIST @@ -1,8 +1,10 @@ -@comment $NetBSD: PLIST,v 1.9 2009/06/14 20:34:13 joerg Exp $ +@comment $NetBSD: PLIST,v 1.10 2009/09/05 20:44:57 tonio Exp $ bin/coq-interface +bin/coq-parser bin/coq-tex bin/coq_makefile bin/coqc +bin/coqchk bin/coqdep bin/coqdoc ${PLIST.coqide}bin/coqide @@ -12,17 +14,89 @@ bin/coqtop bin/coqtop.byte bin/coqwc bin/gallina -bin/parser +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/recdef/Recdef.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 @@ -34,10 +108,20 @@ 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 @@ -53,42 +137,244 @@ 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/subtac/FixSub.vo -lib/coq/contrib/subtac/FunctionalExtensionality.vo -lib/coq/contrib/subtac/Heq.vo -lib/coq/contrib/subtac/Subtac.vo -lib/coq/contrib/subtac/SubtacTactics.vo -lib/coq/contrib/subtac/Utils.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 lib/coq/ide/coq.png -lib/coq/ide/utf8.v -lib/coq/ide/utf8.vo -lib/coq/states/contrib.cma -lib/coq/states/contrib.cmxa -lib/coq/states/highparsing.cma -lib/coq/states/highparsing.cmxa -lib/coq/states/hightactics.cma -lib/coq/states/hightactics.cmxa +lib/coq/interp/constrextern.cmi +lib/coq/interp/constrintern.cmi +lib/coq/interp/coqlib.cmi +lib/coq/interp/dumpglob.cmi +lib/coq/interp/genarg.cmi +lib/coq/interp/implicit_quantifiers.cmi +lib/coq/interp/interp.a +lib/coq/interp/interp.cma +lib/coq/interp/interp.cmxa +lib/coq/interp/modintern.cmi +lib/coq/interp/notation.cmi +lib/coq/interp/ppextend.cmi +lib/coq/interp/reserve.cmi +lib/coq/interp/syntax_def.cmi +lib/coq/interp/topconstr.cmi +lib/coq/kernel/cbytecodes.cmi +lib/coq/kernel/cbytegen.cmi +lib/coq/kernel/cemitcodes.cmi +lib/coq/kernel/closure.cmi +lib/coq/kernel/conv_oracle.cmi +lib/coq/kernel/cooking.cmi +lib/coq/kernel/copcodes.cmi +lib/coq/kernel/csymtable.cmi +lib/coq/kernel/declarations.cmi +lib/coq/kernel/entries.cmi +lib/coq/kernel/environ.cmi +lib/coq/kernel/esubst.cmi +lib/coq/kernel/indtypes.cmi +lib/coq/kernel/inductive.cmi +lib/coq/kernel/kernel.a +lib/coq/kernel/kernel.cma +lib/coq/kernel/kernel.cmxa +lib/coq/kernel/mod_subst.cmi +lib/coq/kernel/mod_typing.cmi +lib/coq/kernel/modops.cmi +lib/coq/kernel/names.cmi +lib/coq/kernel/pre_env.cmi +lib/coq/kernel/reduction.cmi +lib/coq/kernel/retroknowledge.cmi +lib/coq/kernel/safe_typing.cmi +lib/coq/kernel/sign.cmi +lib/coq/kernel/subtyping.cmi +lib/coq/kernel/term.cmi +lib/coq/kernel/term_typing.cmi +lib/coq/kernel/type_errors.cmi +lib/coq/kernel/typeops.cmi +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/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/gmap.cmi +lib/coq/lib/gmapl.cmi +lib/coq/lib/gset.cmi +lib/coq/lib/hashcons.cmi +lib/coq/lib/heap.cmi +lib/coq/lib/lib.a +lib/coq/lib/lib.cma +lib/coq/lib/lib.cmxa +lib/coq/lib/option.cmi +lib/coq/lib/pp.cmi +lib/coq/lib/pp_control.cmi +lib/coq/lib/predicate.cmi +lib/coq/lib/profile.cmi +lib/coq/lib/rtree.cmi +lib/coq/lib/system.cmi +lib/coq/lib/tlm.cmi +lib/coq/lib/util.cmi +lib/coq/libcoqrun.a +lib/coq/library/decl_kinds.cmi +lib/coq/library/declare.cmi +lib/coq/library/declaremods.cmi +lib/coq/library/decls.cmi +lib/coq/library/dischargedhypsmap.cmi +lib/coq/library/global.cmi +lib/coq/library/goptions.cmi +lib/coq/library/heads.cmi +lib/coq/library/impargs.cmi +lib/coq/library/lib.cmi +lib/coq/library/libnames.cmi +lib/coq/library/libobject.cmi +lib/coq/library/library.a +lib/coq/library/library.cma +lib/coq/library/library.cmi +lib/coq/library/library.cmxa +lib/coq/library/nameops.cmi +lib/coq/library/nametab.cmi +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/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 +lib/coq/parsing/highparsing.cmxa +lib/coq/parsing/lexer.cmi +lib/coq/parsing/parsing.a +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/search.cmi +lib/coq/parsing/tactic_printer.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/indrec.cmi +lib/coq/pretyping/inductiveops.cmi +lib/coq/pretyping/matching.cmi +lib/coq/pretyping/pattern.cmi +lib/coq/pretyping/pretype_errors.cmi +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 +lib/coq/pretyping/tacred.cmi +lib/coq/pretyping/termops.cmi +lib/coq/pretyping/typeclasses.cmi +lib/coq/pretyping/typeclasses_errors.cmi +lib/coq/pretyping/typing.cmi +lib/coq/pretyping/unification.cmi +lib/coq/pretyping/vnorm.cmi +lib/coq/proofs/clenvtac.cmi +lib/coq/proofs/decl_mode.cmi +lib/coq/proofs/evar_refiner.cmi +lib/coq/proofs/logic.cmi +lib/coq/proofs/pfedit.cmi +lib/coq/proofs/proof_trees.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/redexpr.cmi +lib/coq/proofs/refiner.cmi +lib/coq/proofs/tacexpr.cmi +lib/coq/proofs/tacmach.cmi +lib/coq/proofs/tactic_debug.cmi lib/coq/states/initial.coq -lib/coq/states/interp.cma -lib/coq/states/interp.cmxa -lib/coq/states/kernel.cma -lib/coq/states/kernel.cmxa -lib/coq/states/lib.cma -lib/coq/states/lib.cmxa -lib/coq/states/library.cma -lib/coq/states/library.cmxa -lib/coq/states/parsing.cma -lib/coq/states/parsing.cmxa -lib/coq/states/pretyping.cma -lib/coq/states/pretyping.cmxa -lib/coq/states/proofs.cma -lib/coq/states/proofs.cmxa -lib/coq/states/tactics.cma -lib/coq/states/tactics.cmxa -lib/coq/states/toplevel.cma -lib/coq/states/toplevel.cmxa +lib/coq/tactics/auto.cmi +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 +lib/coq/tactics/eqdecide.cmi +lib/coq/tactics/equality.cmi +lib/coq/tactics/evar_tactics.cmi +lib/coq/tactics/extraargs.cmi +lib/coq/tactics/extratactics.cmi +lib/coq/tactics/hiddentac.cmi +lib/coq/tactics/hightactics.a +lib/coq/tactics/hightactics.cma +lib/coq/tactics/hightactics.cmxa +lib/coq/tactics/hipattern.cmi +lib/coq/tactics/inv.cmi +lib/coq/tactics/leminv.cmi +lib/coq/tactics/nbtermdn.cmi +lib/coq/tactics/refine.cmi +lib/coq/tactics/tacinterp.cmi +lib/coq/tactics/tacticals.cmi +lib/coq/tactics/tactics.a +lib/coq/tactics/tactics.cma +lib/coq/tactics/tactics.cmi +lib/coq/tactics/tactics.cmxa +lib/coq/tactics/tauto.cmi +lib/coq/tactics/termdn.cmi lib/coq/theories/Arith/Arith.vo lib/coq/theories/Arith/Arith_base.vo lib/coq/theories/Arith/Between.vo @@ -117,30 +403,37 @@ lib/coq/theories/Bool/DecBool.vo lib/coq/theories/Bool/IfProp.vo 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/SetoidClass.vo +lib/coq/theories/Classes/SetoidDec.vo +lib/coq/theories/Classes/SetoidTactics.vo lib/coq/theories/FSets/FMapAVL.vo lib/coq/theories/FSets/FMapFacts.vo -lib/coq/theories/FSets/FMapIntMap.vo +lib/coq/theories/FSets/FMapFullAVL.vo lib/coq/theories/FSets/FMapInterface.vo lib/coq/theories/FSets/FMapList.vo lib/coq/theories/FSets/FMapPositive.vo -lib/coq/theories/FSets/FMapWeak.vo -lib/coq/theories/FSets/FMapWeakFacts.vo -lib/coq/theories/FSets/FMapWeakInterface.vo 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/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/FSetProperties.vo lib/coq/theories/FSets/FSetToFiniteSet.vo -lib/coq/theories/FSets/FSetWeak.vo -lib/coq/theories/FSets/FSetWeakFacts.vo -lib/coq/theories/FSets/FSetWeakInterface.vo lib/coq/theories/FSets/FSetWeakList.vo -lib/coq/theories/FSets/FSetWeakProperties.vo lib/coq/theories/FSets/FSets.vo lib/coq/theories/FSets/OrderedType.vo lib/coq/theories/FSets/OrderedTypeAlt.vo @@ -154,24 +447,12 @@ lib/coq/theories/Init/Prelude.vo lib/coq/theories/Init/Specif.vo lib/coq/theories/Init/Tactics.vo lib/coq/theories/Init/Wf.vo -lib/coq/theories/IntMap/Adalloc.vo -lib/coq/theories/IntMap/Allmaps.vo -lib/coq/theories/IntMap/Fset.vo -lib/coq/theories/IntMap/Lsort.vo -lib/coq/theories/IntMap/Map.vo -lib/coq/theories/IntMap/Mapaxioms.vo -lib/coq/theories/IntMap/Mapc.vo -lib/coq/theories/IntMap/Mapcanon.vo -lib/coq/theories/IntMap/Mapcard.vo -lib/coq/theories/IntMap/Mapfold.vo -lib/coq/theories/IntMap/Mapiter.vo -lib/coq/theories/IntMap/Maplists.vo -lib/coq/theories/IntMap/Mapsubset.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 lib/coq/theories/Lists/TheoryList.vo lib/coq/theories/Logic/Berardi.vo @@ -190,15 +471,20 @@ 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 lib/coq/theories/Logic/Eqdep.vo lib/coq/theories/Logic/EqdepFacts.vo lib/coq/theories/Logic/Eqdep_dec.vo +lib/coq/theories/Logic/FunctionalExtensionality.vo lib/coq/theories/Logic/Hurkens.vo +lib/coq/theories/Logic/IndefiniteDescription.vo lib/coq/theories/Logic/JMeq.vo 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/NArith/BinNat.vo lib/coq/theories/NArith/BinPos.vo lib/coq/theories/NArith/NArith.vo @@ -207,12 +493,83 @@ lib/coq/theories/NArith/Ndigits.vo lib/coq/theories/NArith/Ndist.vo lib/coq/theories/NArith/Nnat.vo lib/coq/theories/NArith/Pnat.vo +lib/coq/theories/Numbers/BigNumPrelude.vo +lib/coq/theories/Numbers/Cyclic/Abstract/CyclicAxioms.vo +lib/coq/theories/Numbers/Cyclic/Abstract/NZCyclic.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.vo +lib/coq/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.vo +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/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/ZLt.vo +lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo +lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.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 +lib/coq/theories/Numbers/Integer/NatPairs/ZNatPairs.vo +lib/coq/theories/Numbers/Integer/SpecViaZ/ZSig.vo +lib/coq/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.vo +lib/coq/theories/Numbers/NaryFunctions.vo +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/NZMul.vo +lib/coq/theories/Numbers/NatInt/NZMulOrder.vo +lib/coq/theories/Numbers/NatInt/NZOrder.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/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/NSub.vo +lib/coq/theories/Numbers/Natural/BigN/BigN.vo +lib/coq/theories/Numbers/Natural/BigN/NMake.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 +lib/coq/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.vo +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/Program/Basics.vo +lib/coq/theories/Program/Combinators.vo +lib/coq/theories/Program/Equality.vo +lib/coq/theories/Program/Program.vo +lib/coq/theories/Program/Subset.vo +lib/coq/theories/Program/Syntax.vo +lib/coq/theories/Program/Tactics.vo +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/Qabs.vo lib/coq/theories/QArith/Qcanon.vo +lib/coq/theories/QArith/Qfield.vo +lib/coq/theories/QArith/Qpower.vo lib/coq/theories/QArith/Qreals.vo lib/coq/theories/QArith/Qreduction.vo lib/coq/theories/QArith/Qring.vo +lib/coq/theories/QArith/Qround.vo lib/coq/theories/Reals/Alembert.vo lib/coq/theories/Reals/AltSeries.vo lib/coq/theories/Reals/ArithProp.vo @@ -250,6 +607,7 @@ lib/coq/theories/Reals/Rgeom.vo 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/Rpow_def.vo lib/coq/theories/Reals/Rpower.vo lib/coq/theories/Reals/Rprod.vo @@ -268,12 +626,10 @@ lib/coq/theories/Reals/SeqSeries.vo lib/coq/theories/Reals/SplitAbsolu.vo lib/coq/theories/Reals/SplitRmult.vo lib/coq/theories/Reals/Sqrt_reg.vo -lib/coq/theories/Relations/Newman.vo lib/coq/theories/Relations/Operators_Properties.vo lib/coq/theories/Relations/Relation_Definitions.vo lib/coq/theories/Relations/Relation_Operators.vo lib/coq/theories/Relations/Relations.vo -lib/coq/theories/Relations/Rstar.vo lib/coq/theories/Setoids/Setoid.vo lib/coq/theories/Sets/Classical_sets.vo lib/coq/theories/Sets/Constructive_sets.vo @@ -304,6 +660,7 @@ lib/coq/theories/Sorting/Permutation.vo lib/coq/theories/Sorting/Sorting.vo lib/coq/theories/Strings/Ascii.vo lib/coq/theories/Strings/String.vo +lib/coq/theories/Unicode/Utf8.vo lib/coq/theories/Wellfounded/Disjoint_Union.vo lib/coq/theories/Wellfounded/Inclusion.vo lib/coq/theories/Wellfounded/Inverse_Image.vo @@ -319,6 +676,8 @@ lib/coq/theories/ZArith/Wf_Z.vo lib/coq/theories/ZArith/ZArith.vo 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/Zabs.vo lib/coq/theories/ZArith/Zbinary.vo lib/coq/theories/ZArith/Zbool.vo @@ -326,6 +685,7 @@ lib/coq/theories/ZArith/Zcompare.vo lib/coq/theories/ZArith/Zcomplements.vo lib/coq/theories/ZArith/Zdiv.vo lib/coq/theories/ZArith/Zeven.vo +lib/coq/theories/ZArith/Zgcd_alt.vo lib/coq/theories/ZArith/Zhints.vo lib/coq/theories/ZArith/Zlogarithm.vo lib/coq/theories/ZArith/Zmax.vo @@ -336,24 +696,51 @@ lib/coq/theories/ZArith/Znat.vo lib/coq/theories/ZArith/Znumtheory.vo lib/coq/theories/ZArith/Zorder.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/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/cerrors.cmi +lib/coq/toplevel/class.cmi +lib/coq/toplevel/classes.cmi +lib/coq/toplevel/command.cmi +lib/coq/toplevel/coqinit.cmi +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/metasyntax.cmi +lib/coq/toplevel/mltop.cmi +lib/coq/toplevel/protectedtoplevel.cmi +lib/coq/toplevel/record.cmi +lib/coq/toplevel/toplevel.a +lib/coq/toplevel/toplevel.cma +lib/coq/toplevel/toplevel.cmi +lib/coq/toplevel/toplevel.cmxa +lib/coq/toplevel/usage.cmi +lib/coq/toplevel/vernac.cmi +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/coqdep.1 man/man1/coqdoc.1 +man/man1/coqide.1 man/man1/coqmktop.1 man/man1/coqtop.1 man/man1/coqtop.byte.1 man/man1/coqwc.1 man/man1/gallina.1 -man/man1/parser.1 share/emacs/site-lisp/coq-inferior.el share/emacs/site-lisp/coq.el share/emacs/site-lisp/coqdoc.sty diff --git a/lang/coq/PLIST.opt b/lang/coq/PLIST.opt index 2464aadaf65..d650b8b8f3f 100644 --- a/lang/coq/PLIST.opt +++ b/lang/coq/PLIST.opt @@ -1,6 +1,7 @@ -@comment $NetBSD: PLIST.opt,v 1.5 2008/04/27 10:46:16 tonio Exp $ +@comment $NetBSD: PLIST.opt,v 1.6 2009/09/05 20:44:57 tonio Exp $ bin/coq-interface.opt +bin/coq-parser.opt +bin/coqchk.opt ${PLIST.coqide}bin/coqide.opt bin/coqtop.opt -bin/parser.opt man/man1/coqtop.opt.1 diff --git a/lang/coq/distinfo b/lang/coq/distinfo index 7ed6e1723e1..7934cf35172 100644 --- a/lang/coq/distinfo +++ b/lang/coq/distinfo @@ -1,7 +1,8 @@ -$NetBSD: distinfo,v 1.8 2008/01/12 11:48:40 tonio Exp $ +$NetBSD: distinfo,v 1.9 2009/09/05 20:44:58 tonio Exp $ -SHA1 (coq-8.1pl3.tar.gz) = c06141891c2a793ff6b4bc1f106d9477b3a9a52e -RMD160 (coq-8.1pl3.tar.gz) = f8f4749e1014cb47a83915550713cf9ce1992e34 -Size (coq-8.1pl3.tar.gz) = 3003593 bytes -SHA1 (patch-aa) = bdfe2986da84b13c7df383caf969858707be83f3 -SHA1 (patch-ab) = b252096b0bef5fee0a2f719ddc17021fd013ed64 +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) = 6573a11efab6ef7c026e8fd39b23e8596dee5a61 +SHA1 (patch-ac) = 30780c9f96ad16c814a5edc50bd1edbd030aa9b5 diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa index 5f3afb50e2f..026e33168dd 100644 --- a/lang/coq/patches/patch-aa +++ b/lang/coq/patches/patch-aa @@ -1,168 +1,13 @@ -$NetBSD: patch-aa,v 1.7 2008/01/12 11:48:40 tonio Exp $ +$NetBSD: patch-aa,v 1.8 2009/09/05 20:44:58 tonio Exp $ ---- Makefile.orig Mon Nov 12 16:10:25 2007 +--- Makefile.orig 2009-04-08 17:38:39.000000000 +0200 +++ Makefile -@@ -690,22 +690,22 @@ install-coqide:: install-ide-$(HASCOQIDE - install-ide-no: - - install-ide-byte: -- $(MKDIR) $(FULLBINDIR) -- cp $(COQIDEBYTE) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE) - - install-ide-opt: -- $(MKDIR) $(FULLBINDIR) -- cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_SCRIPT} $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) - - install-ide-files: -- $(MKDIR) $(FULLIDELIB) -- cp $(IDEFILES) $(FULLIDELIB) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB) -+ ${BSD_INSTALL_DATA} $(IDEFILES) $(FULLIDELIB) - - install-ide-info: -- $(MKDIR) $(FULLIDELIB) -- cp ide/FAQ $(FULLIDELIB) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLIDELIB) -+ ${BSD_INSTALL_DATA} ide/FAQ $(FULLIDELIB) - +@@ -24,8 +24,6 @@ + # by Emacs' next-error. ########################################################################### - # Pcoq: special binaries for debugging (coq-interface, parser) -@@ -775,18 +775,18 @@ clean:: - install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages - - install-pcoq-binaries:: -- $(MKDIR) $(FULLBINDIR) -- cp $(COQINTERFACE) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM} $(COQINTERFACE) $(FULLBINDIR) - - install-pcoq-files:: -- $(MKDIR) $(FULLCOQLIB)/contrib/interface -- cp $(INTERFACERC) $(FULLCOQLIB)/contrib/interface -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/contrib/interface -+ ${BSD_INSTALL_DATA} $(INTERFACERC) $(FULLCOQLIB)/contrib/interface - - PCOQMANPAGES=man/coq-interface.1 man/parser.1 - - install-pcoq-manpages: -- $(MKDIR) $(FULLMANDIR)/man1 -- cp $(PCOQMANPAGES) $(FULLMANDIR)/man1 -+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1 -+ ${BSD_INSTALL_MAN} $(PCOQMANPAGES) $(FULLMANDIR)/man1 - - ########################################################################### - # tests -@@ -1244,22 +1244,21 @@ install-coqlight: install-binaries insta - install-binaries:: install-$(BEST) install-tools - - install-byte:: -- $(MKDIR) $(FULLBINDIR) -- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE) - - install-opt:: -- $(MKDIR) $(FULLBINDIR) -- cp $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_SCRIPT} $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR) - cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE) - install-tools:: -- $(MKDIR) $(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) -- cp tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc -- cp $(TOOLS) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLBINDIR) -+ ${BSD_INSTALL_SCRIPT} $(TOOLS) $(FULLBINDIR) -+ ${BSD_INSTALL_PROGRAM_DIR} $(FULLCOQLIB)/tools/coqdoc -+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc - - LIBFILES=$(THEORIESVO) $(CONTRIBVO) - LIBFILESLIGHT=$(THEORIESLIGHTVO) -@@ -1274,52 +1273,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma - OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa) - - install-library: -- $(MKDIR) $(FULLCOQLIB) -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB) - for f in $(LIBFILES); do \ -- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ -- cp $$f $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \ - done -- $(MKDIR) $(FULLCOQLIB)/states -- cp states/*.coq $(FULLCOQLIB)/states -- $(MKDIR) $(FULLCOQLIB)/user-contrib -- cp $(OBJECTCMA) $(OBJECTCMXA) $(GRAMMARCMA) $(FULLCOQLIB) -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states -+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/user-contrib -+ ${BSD_INSTALL_DATA} $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB)/states - - install-library-light: -- $(MKDIR) $(FULLCOQLIB) -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB) - for f in $(LIBFILESLIGHT); do \ -- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ -- cp $$f $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \ - done -- $(MKDIR) $(FULLCOQLIB)/states -- cp states/*.coq $(FULLCOQLIB)/states -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states -+ ${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states - - install-allreals:: - for f in $(ALLREALS); do \ -- $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \ -- cp $$f $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \ -+ ${BSD_INSTALL_DATA} $$f $(FULLCOQLIB)/`dirname $$f`; \ - done - - install-coq-info: install-coq-manpages install-emacs install-latex - - MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ -- man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ -+ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 \ - man/coqwc.1 man/coqdoc.1 \ - man/coq_makefile.1 man/coqmktop.1 -+ ifeq ($(BEST),opt) -+ MANPAGES+=man/coqtop.opt.1 -+ endif - - install-coq-manpages: -- $(MKDIR) $(FULLMANDIR)/man1 -- cp $(MANPAGES) $(FULLMANDIR)/man1 -+ ${BSD_INSTALL_DATA_DIR} $(FULLMANDIR)/man1 -+ ${BSD_INSTALL_MAN} $(MANPAGES) $(FULLMANDIR)/man1 - - install-emacs: -- $(MKDIR) $(FULLEMACSLIB) -- cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB) -+ ${BSD_INSTALL_DATA_DIR} $(FULLEMACSLIB) -+ ${BSD_INSTALL_DATA} tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB) - - # command to update TeX' kpathsea database - #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null - - install-latex: -- $(MKDIR) $(FULLCOQDOCDIR) -- cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) -+ ${BSD_INSTALL_DATA_DIR} $(FULLCOQDOCDIR) -+ ${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR) - # -$(UPDATETEX) - - ########################################################################### +-export SHELL:=/bin/bash +- + export FIND_VCS_CLAUSE:='(' \ + -name '{arch}' -o \ + -name '.svn' -o \ diff --git a/lang/coq/patches/patch-ab b/lang/coq/patches/patch-ab index 60630877b49..0ed17e25bef 100644 --- a/lang/coq/patches/patch-ab +++ b/lang/coq/patches/patch-ab @@ -1,13 +1,22 @@ -$NetBSD: patch-ab,v 1.1 2007/12/01 13:05:37 tonio Exp $ +$NetBSD: patch-ab,v 1.2 2009/09/05 20:44:58 tonio Exp $ ---- configure.orig Thu Oct 11 15:13:51 2007 +--- configure.orig 2009-07-01 11:58:00.000000000 +0200 +++ configure -@@ -326,7 +326,7 @@ esac +@@ -331,7 +331,7 @@ if [ "$MAKE" != "" ]; then + 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 +412,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" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` + CAMLVERSION=`"$bytecamlc" -version` diff --git a/lang/coq/patches/patch-ac b/lang/coq/patches/patch-ac new file mode 100644 index 00000000000..1ac85f2dfb2 --- /dev/null +++ b/lang/coq/patches/patch-ac @@ -0,0 +1,12 @@ +$NetBSD: patch-ac,v 1.1 2009/09/05 20:44:58 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 |