Update lang/coq to 8.1

Many changes, among them:
- Many bugs have been fixed (cf coq-bugs web page)
- changed parsing precedence of let/in and fun constructions of Ltac:
  let x := t in e1; e2 is now parsed as let x := t in (e1;e2).
- New primitive "external" for communication with tool external to Coq.
- Omega now handles arbitrary precision integers.
- Haskell extraction: types of functions are now printed, better
  unsafeCoerce mechanism, both for hugs and ghc.
- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme.
- New notation "exists! x:A, P" for unique existence.
- New library on String and Ascii characters (contributed by L. Thery).
- New library FSets+FMaps of finite sets and maps.
- New library QArith on rational numbers.
- Few improvements in ZArith potentially exceptionally breaking the
  compatibility (useless hypothesys of Zgt_square_simpl and
  Zlt_square_simpl removed; fixed names mentioning letter O instead of
  digit 0; weaken premises in Z_lt_induction).

4 files changed, 160 insertions, 306 deletions

diff --git a/lang/coq/Makefile b/lang/coq/Makefile
index 530dab2c324..553df998aea 100644
--- a/lang/coq/Makefile
+++ b/lang/coq/Makefile
@@ -1,10 +1,9 @@
-# $NetBSD: Makefile,v 1.15 2007/01/17 11:14:46 tonio Exp $
+# $NetBSD: Makefile,v 1.16 2007/02/25 15:03:52 tonio Exp $
 #
 
-DISTNAME=	coq-8.0pl3
-PKGREVISION=	1
+DISTNAME=	coq-8.1
 CATEGORIES=	lang math
-MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/
+MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V8.1/
 
 MAINTAINER=	richards+netbsd@CS.Princeton.EDU
 HOMEPAGE=	http://coq.inria.fr/
@@ -22,7 +21,7 @@ BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=3.09
 .include "../../mk/bsd.prefs.mk"
 
 .if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "powerpc") || \
-	(${MACHINE_ARCH} == "sparc")
+	(${MACHINE_ARCH} == "sparc") || (${MACHINE_ARCH} == "x86_64")
 PLIST_SRC=	${PKGDIR}/PLIST.opt ${PKGDIR}/PLIST
 .endif
 
diff --git a/lang/coq/PLIST b/lang/coq/PLIST
index 0469c4833b8..cd61278a593 100644
--- a/lang/coq/PLIST
+++ b/lang/coq/PLIST
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.4 2007/01/17 11:14:46 tonio Exp $
+@comment $NetBSD: PLIST,v 1.5 2007/02/25 15:03:52 tonio Exp $
 bin/coq-interface
 bin/coq-tex
 bin/coq_makefile
@@ -13,61 +13,82 @@ bin/coqtop.byte
 bin/coqwc
 bin/gallina
 bin/parser
-lib/coq/contrib/cc/CCSolve.vo
-lib/coq/contrib/field/Field.vo
-lib/coq/contrib/field/Field_Compl.vo
-lib/coq/contrib/field/Field_Tactic.vo
-lib/coq/contrib/field/Field_Theory.vo
+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/fourier/Fourier.vo
 lib/coq/contrib/fourier/Fourier_util.vo
 lib/coq/contrib/interface/vernacrc
 lib/coq/contrib/omega/Omega.vo
 lib/coq/contrib/omega/OmegaLemmas.vo
-lib/coq/contrib/ring/ArithRing.vo
-lib/coq/contrib/ring/NArithRing.vo
+lib/coq/contrib/recdef/Recdef.vo
+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.vo
 lib/coq/contrib/ring/Ring_abstract.vo
 lib/coq/contrib/ring/Ring_normalize.vo
-lib/coq/contrib/ring/Ring_theory.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/ZArithRing.vo
 lib/coq/contrib/romega/ROmega.vo
 lib/coq/contrib/romega/ReflOmegaCore.vo
-lib/coq/contrib7/cc/CCSolve.vo
-lib/coq/contrib7/field/Field.vo
-lib/coq/contrib7/field/Field_Compl.vo
-lib/coq/contrib7/field/Field_Tactic.vo
-lib/coq/contrib7/field/Field_Theory.vo
-lib/coq/contrib7/fourier/Fourier.vo
-lib/coq/contrib7/fourier/Fourier_util.vo
-lib/coq/contrib7/omega/Omega.vo
-lib/coq/contrib7/omega/OmegaLemmas.vo
-lib/coq/contrib7/ring/ArithRing.vo
-lib/coq/contrib7/ring/NArithRing.vo
-lib/coq/contrib7/ring/Quote.vo
-lib/coq/contrib7/ring/Ring.vo
-lib/coq/contrib7/ring/Ring_abstract.vo
-lib/coq/contrib7/ring/Ring_normalize.vo
-lib/coq/contrib7/ring/Ring_theory.vo
-lib/coq/contrib7/ring/Setoid_ring.vo
-lib/coq/contrib7/ring/Setoid_ring_normalize.vo
-lib/coq/contrib7/ring/Setoid_ring_theory.vo
-lib/coq/contrib7/ring/ZArithRing.vo
-lib/coq/contrib7/romega/ROmega.vo
-lib/coq/contrib7/romega/ReflOmegaCore.vo
+lib/coq/contrib/rtauto/Bintree.vo
+lib/coq/contrib/rtauto/Rtauto.vo
+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/subtac/FixSub.vo
+lib/coq/contrib/subtac/FunctionalExtensionality.vo
+lib/coq/contrib/subtac/Subtac.vo
+lib/coq/contrib/subtac/Utils.vo
 lib/coq/ide/.coqide-gtk2rc
 lib/coq/ide/FAQ
-lib/coq/ide/coq.ico
-lib/coq/ide/coq2.ico
+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/states/initial.coq
-lib/coq/states7/barestate.coq
-lib/coq/states7/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/theories/Arith/Arith.vo
+lib/coq/theories/Arith/Arith_base.vo
 lib/coq/theories/Arith/Between.vo
 lib/coq/theories/Arith/Bool_nat.vo
 lib/coq/theories/Arith/Compare.vo
@@ -94,6 +115,34 @@ 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/FSets/FMapAVL.vo
+lib/coq/theories/FSets/FMapFacts.vo
+lib/coq/theories/FSets/FMapIntMap.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/FSetEqProperties.vo
+lib/coq/theories/FSets/FSetFacts.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
+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
@@ -101,11 +150,9 @@ lib/coq/theories/Init/Notations.vo
 lib/coq/theories/Init/Peano.vo
 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/Addec.vo
-lib/coq/theories/IntMap/Addr.vo
-lib/coq/theories/IntMap/Adist.vo
 lib/coq/theories/IntMap/Allmaps.vo
 lib/coq/theories/IntMap/Fset.vo
 lib/coq/theories/IntMap/Lsort.vo
@@ -120,7 +167,9 @@ 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/Streams.vo
 lib/coq/theories/Lists/TheoryList.vo
 lib/coq/theories/Logic/Berardi.vo
@@ -128,23 +177,40 @@ lib/coq/theories/Logic/ChoiceFacts.vo
 lib/coq/theories/Logic/Classical.vo
 lib/coq/theories/Logic/ClassicalChoice.vo
 lib/coq/theories/Logic/ClassicalDescription.vo
+lib/coq/theories/Logic/ClassicalEpsilon.vo
 lib/coq/theories/Logic/ClassicalFacts.vo
+lib/coq/theories/Logic/ClassicalUniqueChoice.vo
 lib/coq/theories/Logic/Classical_Pred_Set.vo
 lib/coq/theories/Logic/Classical_Pred_Type.vo
 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/Diaconescu.vo
 lib/coq/theories/Logic/Eqdep.vo
+lib/coq/theories/Logic/EqdepFacts.vo
 lib/coq/theories/Logic/Eqdep_dec.vo
 lib/coq/theories/Logic/Hurkens.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/NArith/BinNat.vo
 lib/coq/theories/NArith/BinPos.vo
 lib/coq/theories/NArith/NArith.vo
+lib/coq/theories/NArith/Ndec.vo
+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/QArith/QArith.vo
+lib/coq/theories/QArith/QArith_base.vo
+lib/coq/theories/QArith/Qcanon.vo
+lib/coq/theories/QArith/Qreals.vo
+lib/coq/theories/QArith/Qreduction.vo
+lib/coq/theories/QArith/Qring.vo
 lib/coq/theories/Reals/Alembert.vo
 lib/coq/theories/Reals/AltSeries.vo
 lib/coq/theories/Reals/ArithProp.vo
@@ -155,6 +221,7 @@ lib/coq/theories/Reals/Cos_rel.vo
 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/MVT.vo
 lib/coq/theories/Reals/NewtonInt.vo
 lib/coq/theories/Reals/PSeries_reg.vo
@@ -181,6 +248,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/Rpow_def.vo
 lib/coq/theories/Reals/Rpower.vo
 lib/coq/theories/Reals/Rprod.vo
 lib/coq/theories/Reals/Rseries.vo
@@ -228,8 +296,12 @@ 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/PermutEq.vo
+lib/coq/theories/Sorting/PermutSetoid.vo
 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/Wellfounded/Disjoint_Union.vo
 lib/coq/theories/Wellfounded/Inclusion.vo
 lib/coq/theories/Wellfounded/Inverse_Image.vo
@@ -240,6 +312,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/Int.vo
 lib/coq/theories/ZArith/Wf_Z.vo
 lib/coq/theories/ZArith/ZArith.vo
 lib/coq/theories/ZArith/ZArith_base.vo
@@ -253,216 +326,20 @@ lib/coq/theories/ZArith/Zdiv.vo
 lib/coq/theories/ZArith/Zeven.vo
 lib/coq/theories/ZArith/Zhints.vo
 lib/coq/theories/ZArith/Zlogarithm.vo
+lib/coq/theories/ZArith/Zmax.vo
 lib/coq/theories/ZArith/Zmin.vo
+lib/coq/theories/ZArith/Zminmax.vo
 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_def.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/theories7/Arith/Arith.vo
-lib/coq/theories7/Arith/Between.vo
-lib/coq/theories7/Arith/Bool_nat.vo
-lib/coq/theories7/Arith/Compare.vo
-lib/coq/theories7/Arith/Compare_dec.vo
-lib/coq/theories7/Arith/Div2.vo
-lib/coq/theories7/Arith/EqNat.vo
-lib/coq/theories7/Arith/Euclid.vo
-lib/coq/theories7/Arith/Even.vo
-lib/coq/theories7/Arith/Factorial.vo
-lib/coq/theories7/Arith/Gt.vo
-lib/coq/theories7/Arith/Le.vo
-lib/coq/theories7/Arith/Lt.vo
-lib/coq/theories7/Arith/Max.vo
-lib/coq/theories7/Arith/Min.vo
-lib/coq/theories7/Arith/Minus.vo
-lib/coq/theories7/Arith/Mult.vo
-lib/coq/theories7/Arith/Peano_dec.vo
-lib/coq/theories7/Arith/Plus.vo
-lib/coq/theories7/Arith/Wf_nat.vo
-lib/coq/theories7/Bool/Bool.vo
-lib/coq/theories7/Bool/BoolEq.vo
-lib/coq/theories7/Bool/Bvector.vo
-lib/coq/theories7/Bool/DecBool.vo
-lib/coq/theories7/Bool/IfProp.vo
-lib/coq/theories7/Bool/Sumbool.vo
-lib/coq/theories7/Bool/Zerob.vo
-lib/coq/theories7/Init/Datatypes.vo
-lib/coq/theories7/Init/Logic.vo
-lib/coq/theories7/Init/Logic_Type.vo
-lib/coq/theories7/Init/Notations.vo
-lib/coq/theories7/Init/Peano.vo
-lib/coq/theories7/Init/Prelude.vo
-lib/coq/theories7/Init/Specif.vo
-lib/coq/theories7/Init/Wf.vo
-lib/coq/theories7/IntMap/Adalloc.vo
-lib/coq/theories7/IntMap/Addec.vo
-lib/coq/theories7/IntMap/Addr.vo
-lib/coq/theories7/IntMap/Adist.vo
-lib/coq/theories7/IntMap/Allmaps.vo
-lib/coq/theories7/IntMap/Fset.vo
-lib/coq/theories7/IntMap/Lsort.vo
-lib/coq/theories7/IntMap/Map.vo
-lib/coq/theories7/IntMap/Mapaxioms.vo
-lib/coq/theories7/IntMap/Mapc.vo
-lib/coq/theories7/IntMap/Mapcanon.vo
-lib/coq/theories7/IntMap/Mapcard.vo
-lib/coq/theories7/IntMap/Mapfold.vo
-lib/coq/theories7/IntMap/Mapiter.vo
-lib/coq/theories7/IntMap/Maplists.vo
-lib/coq/theories7/IntMap/Mapsubset.vo
-lib/coq/theories7/Lists/List.vo
-lib/coq/theories7/Lists/ListSet.vo
-lib/coq/theories7/Lists/MonoList.vo
-lib/coq/theories7/Lists/PolyList.vo
-lib/coq/theories7/Lists/PolyListSyntax.vo
-lib/coq/theories7/Lists/Streams.vo
-lib/coq/theories7/Lists/TheoryList.vo
-lib/coq/theories7/Logic/Berardi.vo
-lib/coq/theories7/Logic/ChoiceFacts.vo
-lib/coq/theories7/Logic/Classical.vo
-lib/coq/theories7/Logic/ClassicalChoice.vo
-lib/coq/theories7/Logic/ClassicalDescription.vo
-lib/coq/theories7/Logic/ClassicalFacts.vo
-lib/coq/theories7/Logic/Classical_Pred_Set.vo
-lib/coq/theories7/Logic/Classical_Pred_Type.vo
-lib/coq/theories7/Logic/Classical_Prop.vo
-lib/coq/theories7/Logic/Classical_Type.vo
-lib/coq/theories7/Logic/Decidable.vo
-lib/coq/theories7/Logic/Diaconescu.vo
-lib/coq/theories7/Logic/Eqdep.vo
-lib/coq/theories7/Logic/Eqdep_dec.vo
-lib/coq/theories7/Logic/Hurkens.vo
-lib/coq/theories7/Logic/JMeq.vo
-lib/coq/theories7/Logic/ProofIrrelevance.vo
-lib/coq/theories7/Logic/RelationalChoice.vo
-lib/coq/theories7/NArith/BinNat.vo
-lib/coq/theories7/NArith/BinPos.vo
-lib/coq/theories7/NArith/NArith.vo
-lib/coq/theories7/NArith/Pnat.vo
-lib/coq/theories7/Reals/Alembert.vo
-lib/coq/theories7/Reals/AltSeries.vo
-lib/coq/theories7/Reals/ArithProp.vo
-lib/coq/theories7/Reals/Binomial.vo
-lib/coq/theories7/Reals/Cauchy_prod.vo
-lib/coq/theories7/Reals/Cos_plus.vo
-lib/coq/theories7/Reals/Cos_rel.vo
-lib/coq/theories7/Reals/DiscrR.vo
-lib/coq/theories7/Reals/Exp_prop.vo
-lib/coq/theories7/Reals/Integration.vo
-lib/coq/theories7/Reals/MVT.vo
-lib/coq/theories7/Reals/NewtonInt.vo
-lib/coq/theories7/Reals/PSeries_reg.vo
-lib/coq/theories7/Reals/PartSum.vo
-lib/coq/theories7/Reals/RIneq.vo
-lib/coq/theories7/Reals/RList.vo
-lib/coq/theories7/Reals/R_Ifp.vo
-lib/coq/theories7/Reals/R_sqr.vo
-lib/coq/theories7/Reals/R_sqrt.vo
-lib/coq/theories7/Reals/Ranalysis.vo
-lib/coq/theories7/Reals/Ranalysis1.vo
-lib/coq/theories7/Reals/Ranalysis2.vo
-lib/coq/theories7/Reals/Ranalysis3.vo
-lib/coq/theories7/Reals/Ranalysis4.vo
-lib/coq/theories7/Reals/Raxioms.vo
-lib/coq/theories7/Reals/Rbase.vo
-lib/coq/theories7/Reals/Rbasic_fun.vo
-lib/coq/theories7/Reals/Rcomplete.vo
-lib/coq/theories7/Reals/Rdefinitions.vo
-lib/coq/theories7/Reals/Rderiv.vo
-lib/coq/theories7/Reals/Reals.vo
-lib/coq/theories7/Reals/Rfunctions.vo
-lib/coq/theories7/Reals/Rgeom.vo
-lib/coq/theories7/Reals/RiemannInt.vo
-lib/coq/theories7/Reals/RiemannInt_SF.vo
-lib/coq/theories7/Reals/Rlimit.vo
-lib/coq/theories7/Reals/Rpower.vo
-lib/coq/theories7/Reals/Rprod.vo
-lib/coq/theories7/Reals/Rseries.vo
-lib/coq/theories7/Reals/Rsigma.vo
-lib/coq/theories7/Reals/Rsqrt_def.vo
-lib/coq/theories7/Reals/Rsyntax.vo
-lib/coq/theories7/Reals/Rtopology.vo
-lib/coq/theories7/Reals/Rtrigo.vo
-lib/coq/theories7/Reals/Rtrigo_alt.vo
-lib/coq/theories7/Reals/Rtrigo_calc.vo
-lib/coq/theories7/Reals/Rtrigo_def.vo
-lib/coq/theories7/Reals/Rtrigo_fun.vo
-lib/coq/theories7/Reals/Rtrigo_reg.vo
-lib/coq/theories7/Reals/SeqProp.vo
-lib/coq/theories7/Reals/SeqSeries.vo
-lib/coq/theories7/Reals/SplitAbsolu.vo
-lib/coq/theories7/Reals/SplitRmult.vo
-lib/coq/theories7/Reals/Sqrt_reg.vo
-lib/coq/theories7/Relations/Newman.vo
-lib/coq/theories7/Relations/Operators_Properties.vo
-lib/coq/theories7/Relations/Relation_Definitions.vo
-lib/coq/theories7/Relations/Relation_Operators.vo
-lib/coq/theories7/Relations/Relations.vo
-lib/coq/theories7/Relations/Rstar.vo
-lib/coq/theories7/Setoids/Setoid.vo
-lib/coq/theories7/Sets/Classical_sets.vo
-lib/coq/theories7/Sets/Constructive_sets.vo
-lib/coq/theories7/Sets/Cpo.vo
-lib/coq/theories7/Sets/Ensembles.vo
-lib/coq/theories7/Sets/Finite_sets.vo
-lib/coq/theories7/Sets/Finite_sets_facts.vo
-lib/coq/theories7/Sets/Image.vo
-lib/coq/theories7/Sets/Infinite_sets.vo
-lib/coq/theories7/Sets/Integers.vo
-lib/coq/theories7/Sets/Multiset.vo
-lib/coq/theories7/Sets/Partial_Order.vo
-lib/coq/theories7/Sets/Permut.vo
-lib/coq/theories7/Sets/Powerset.vo
-lib/coq/theories7/Sets/Powerset_Classical_facts.vo
-lib/coq/theories7/Sets/Powerset_facts.vo
-lib/coq/theories7/Sets/Relations_1.vo
-lib/coq/theories7/Sets/Relations_1_facts.vo
-lib/coq/theories7/Sets/Relations_2.vo
-lib/coq/theories7/Sets/Relations_2_facts.vo
-lib/coq/theories7/Sets/Relations_3.vo
-lib/coq/theories7/Sets/Relations_3_facts.vo
-lib/coq/theories7/Sets/Uniset.vo
-lib/coq/theories7/Sorting/Heap.vo
-lib/coq/theories7/Sorting/Permutation.vo
-lib/coq/theories7/Sorting/Sorting.vo
-lib/coq/theories7/Wellfounded/Disjoint_Union.vo
-lib/coq/theories7/Wellfounded/Inclusion.vo
-lib/coq/theories7/Wellfounded/Inverse_Image.vo
-lib/coq/theories7/Wellfounded/Lexicographic_Exponentiation.vo
-lib/coq/theories7/Wellfounded/Lexicographic_Product.vo
-lib/coq/theories7/Wellfounded/Transitive_Closure.vo
-lib/coq/theories7/Wellfounded/Union.vo
-lib/coq/theories7/Wellfounded/Well_Ordering.vo
-lib/coq/theories7/Wellfounded/Wellfounded.vo
-lib/coq/theories7/ZArith/BinInt.vo
-lib/coq/theories7/ZArith/Wf_Z.vo
-lib/coq/theories7/ZArith/ZArith.vo
-lib/coq/theories7/ZArith/ZArith_base.vo
-lib/coq/theories7/ZArith/ZArith_dec.vo
-lib/coq/theories7/ZArith/Zabs.vo
-lib/coq/theories7/ZArith/Zbinary.vo
-lib/coq/theories7/ZArith/Zbool.vo
-lib/coq/theories7/ZArith/Zcompare.vo
-lib/coq/theories7/ZArith/Zcomplements.vo
-lib/coq/theories7/ZArith/Zdiv.vo
-lib/coq/theories7/ZArith/Zeven.vo
-lib/coq/theories7/ZArith/Zhints.vo
-lib/coq/theories7/ZArith/Zlogarithm.vo
-lib/coq/theories7/ZArith/Zmin.vo
-lib/coq/theories7/ZArith/Zmisc.vo
-lib/coq/theories7/ZArith/Znat.vo
-lib/coq/theories7/ZArith/Znumtheory.vo
-lib/coq/theories7/ZArith/Zorder.vo
-lib/coq/theories7/ZArith/Zpower.vo
-lib/coq/theories7/ZArith/Zsqrt.vo
-lib/coq/theories7/ZArith/Zsyntax.vo
-lib/coq/theories7/ZArith/Zwf.vo
-lib/coq/theories7/ZArith/auxiliary.vo
-lib/coq/theories7/ZArith/fast_integer.vo
-lib/coq/theories7/ZArith/zarith_aux.vo
+lib/coq/tools/coqdoc/coqdoc.css
+lib/coq/tools/coqdoc/coqdoc.sty
 man/man1/coq-interface.1
 man/man1/coq-tex.1
 man/man1/coq_makefile.1
@@ -478,52 +355,39 @@ man/man1/parser.1
 share/emacs/site-lisp/coq-inferior.el
 share/emacs/site-lisp/coq.el
 share/emacs/site-lisp/coqdoc.sty
-@dirrm lib/coq/theories7/ZArith
-@dirrm lib/coq/theories7/Wellfounded
-@dirrm lib/coq/theories7/Sorting
-@dirrm lib/coq/theories7/Sets
-@dirrm lib/coq/theories7/Setoids
-@dirrm lib/coq/theories7/Relations
-@dirrm lib/coq/theories7/Reals
-@dirrm lib/coq/theories7/NArith
-@dirrm lib/coq/theories7/Logic
-@dirrm lib/coq/theories7/Lists
-@dirrm lib/coq/theories7/IntMap
-@dirrm lib/coq/theories7/Init
-@dirrm lib/coq/theories7/Bool
-@dirrm lib/coq/theories7/Arith
-@dirrm lib/coq/theories7
+@exec ${MKDIR} %D/lib/coq/user-contrib
+@dirrm lib/coq/user-contrib
+@dirrm lib/coq/tools/coqdoc
+@dirrm lib/coq/tools
 @dirrm lib/coq/theories/ZArith
 @dirrm lib/coq/theories/Wellfounded
+@dirrm lib/coq/theories/Strings
 @dirrm lib/coq/theories/Sorting
 @dirrm lib/coq/theories/Sets
 @dirrm lib/coq/theories/Setoids
 @dirrm lib/coq/theories/Relations
 @dirrm lib/coq/theories/Reals
+@dirrm lib/coq/theories/QArith
 @dirrm lib/coq/theories/NArith
 @dirrm lib/coq/theories/Logic
 @dirrm lib/coq/theories/Lists
 @dirrm lib/coq/theories/IntMap
 @dirrm lib/coq/theories/Init
+@dirrm lib/coq/theories/FSets
 @dirrm lib/coq/theories/Bool
 @dirrm lib/coq/theories/Arith
 @dirrm lib/coq/theories
-@dirrm lib/coq/states7
 @dirrm lib/coq/states
 @dirrm lib/coq/ide
-@dirrm lib/coq/contrib7/romega
-@dirrm lib/coq/contrib7/ring
-@dirrm lib/coq/contrib7/omega
-@dirrm lib/coq/contrib7/fourier
-@dirrm lib/coq/contrib7/field
-@dirrm lib/coq/contrib7/cc
-@dirrm lib/coq/contrib7
+@dirrm lib/coq/contrib/subtac
+@dirrm lib/coq/contrib/setoid_ring
+@dirrm lib/coq/contrib/rtauto
 @dirrm lib/coq/contrib/romega
 @dirrm lib/coq/contrib/ring
+@dirrm lib/coq/contrib/recdef
 @dirrm lib/coq/contrib/omega
 @dirrm lib/coq/contrib/interface
 @dirrm lib/coq/contrib/fourier
 @dirrm lib/coq/contrib/field
-@dirrm lib/coq/contrib/cc
 @dirrm lib/coq/contrib
 @dirrm lib/coq
diff --git a/lang/coq/distinfo b/lang/coq/distinfo
index f0c8add20b4..46bce0304cc 100644
--- a/lang/coq/distinfo
+++ b/lang/coq/distinfo
@@ -1,6 +1,6 @@
-$NetBSD: distinfo,v 1.5 2006/01/27 19:22:58 tonio Exp $
+$NetBSD: distinfo,v 1.6 2007/02/25 15:03:52 tonio Exp $
 
-SHA1 (coq-8.0pl3.tar.gz) = b182f25b8e6591139281f7078d049aaa7f0408d8
-RMD160 (coq-8.0pl3.tar.gz) = 925a65fdd0c96f4fe6082bc7bfb8483c83b5fea7
-Size (coq-8.0pl3.tar.gz) = 2309002 bytes
-SHA1 (patch-aa) = 2ef8be34bd9c77229ef9a2a6e5d04891d7e159da
+SHA1 (coq-8.1.tar.gz) = 151aca5b7c919eeb39ba3c6fecec836b7953b206
+RMD160 (coq-8.1.tar.gz) = 548d2e25e7813567252f9b176f318619a780d729
+Size (coq-8.1.tar.gz) = 2977142 bytes
+SHA1 (patch-aa) = 4cc1fdee8074aaa3d1af24151c2d2277522ec9bc
diff --git a/lang/coq/patches/patch-aa b/lang/coq/patches/patch-aa
index a5439a89bd3..2216aff94f0 100644
--- a/lang/coq/patches/patch-aa
+++ b/lang/coq/patches/patch-aa
@@ -1,8 +1,8 @@
-$NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
+$NetBSD: patch-aa,v 1.5 2007/02/25 15:03:52 tonio Exp $
 
---- Makefile.orig	2006-01-12 00:18:05.000000000 +0100
+--- Makefile.orig	2007-02-07 13:21:01.000000000 +0100
 +++ Makefile
-@@ -609,22 +609,22 @@ install-coqide:: install-ide-$(HASCOQIDE
+@@ -697,22 +697,22 @@ install-coqide:: install-ide-$(HASCOQIDE
  install-ide-no:
  
  install-ide-byte: 
@@ -33,7 +33,7 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
  
  ###########################################################################
  # Pcoq: special binaries for debugging (coq-interface, parser)
-@@ -699,18 +699,18 @@ contrib7/interface/AddDad.vo: contrib7/i
+@@ -782,18 +782,18 @@ clean::
  install-pcoq:: install-pcoq-binaries install-pcoq-files install-pcoq-manpages
  
  install-pcoq-binaries::
@@ -58,7 +58,7 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
  
  ###########################################################################
  # tests
-@@ -1139,18 +1139,18 @@ install-coqlight: install-binaries insta
+@@ -1248,21 +1248,21 @@ install-coqlight: install-binaries insta
  install-binaries:: install-$(BEST) install-tools
  
  install-byte::
@@ -77,19 +77,24 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
  
  install-tools::
 -	$(MKDIR) $(FULLBINDIR)
+ 	# recopie des fichiers de style pour coqide
+-	$(MKDIR) $(FULLCOQLIB)/tools/coqdoc
+-	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=$(OLDTHEORIESVO) $(OLDCONTRIBVO)
- LIBFILESLIGHT=$(OLDTHEORIESLIGHTVO)
-@@ -1161,61 +1161,64 @@ NEWLIBFILESLIGHT=$(NEWTHEORIESLIGHTVO)
- install-library: install-library7 install-library8
+ LIBFILES=$(THEORIESVO) $(CONTRIBVO)
+ LIBFILESLIGHT=$(THEORIESLIGHTVO)
+@@ -1275,52 +1275,55 @@ OBJECTCMA=lib/lib.cma kernel/kernel.cma 
+ OBJECTCMXA=$(OBJECTCMA:.cma=.cmxa)
  
- install-library8:
+ install-library:
 -	$(MKDIR) $(FULLCOQLIB)
 +	${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)
- 	for f in $(NEWLIBFILES); do \
+ 	for f in $(LIBFILES); do \
 -	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
 -	  cp $$f $(FULLCOQLIB)/`dirname $$f`; \
 +	  ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
@@ -97,27 +102,17 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
          done
 -	$(MKDIR) $(FULLCOQLIB)/states
 -	cp states/*.coq $(FULLCOQLIB)/states
+-	$(MKDIR) $(FULLCOQLIB)/user-contrib
+-	cp $(OBJECTCMA) $(OBJECTCMXA) $(FULLCOQLIB)
 +	${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
 +	${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
- 
- install-library7:
--	$(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)/states7
--	cp states7/*.coq $(FULLCOQLIB)/states7
-+	${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states7
-+	${BSD_INSTALL_DATA} states7/*.coq $(FULLCOQLIB)/states7
++	${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) $(NEWLIBFILESLIGHT); do \
+ 	for f in $(LIBFILESLIGHT); do \
 -	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
 -	  cp $$f $(FULLCOQLIB)/`dirname $$f`; \
 +	  ${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/`dirname $$f`; \
@@ -125,12 +120,8 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
          done
 -	$(MKDIR) $(FULLCOQLIB)/states
 -	cp states/*.coq $(FULLCOQLIB)/states
--	$(MKDIR) $(FULLCOQLIB)/states7
--	cp states7/*.coq $(FULLCOQLIB)/states7
 +	${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states
 +	${BSD_INSTALL_DATA} states/*.coq $(FULLCOQLIB)/states
-+	${BSD_INSTALL_DATA_DIR} $(FULLCOQLIB)/states7
-+	${BSD_INSTALL_DATA} states7/*.coq $(FULLCOQLIB)/states7
  
  install-allreals::
  	for f in $(ALLREALS); do \
@@ -168,7 +159,7 @@ $NetBSD: patch-aa,v 1.4 2006/01/27 19:22:58 tonio Exp $
  
  install-latex:
 -	$(MKDIR) $(FULLCOQDOCDIR)
--	cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)
+-	cp tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
 +	${BSD_INSTALL_DATA_DIR} $(FULLCOQDOCDIR)
 +	${BSD_INSTALL_DATA} tools/coqdoc/coqdoc.sty $(FULLCOQDOCDIR)	
  #	-$(UPDATETEX)