Update to 7.3.1 and unbreak.
From: Yozo Toda <yozo@v007.vaio.ne.jp>
This commit is contained in:
naddy
parent
55ab8ca501
commit
6cfb0e81a0
@ -1,8 +1,8 @@
|
||||
# $OpenBSD: Makefile,v 1.4 2002/09/07 23:43:09 naddy Exp $
|
||||
# $OpenBSD: Makefile,v 1.5 2002/11/04 21:10:44 naddy Exp $
|
||||
|
||||
COMMENT= "proof assistant based on a typed lambda calculus"
|
||||
|
||||
DISTNAME= coq-7.0
|
||||
DISTNAME= coq-7.3.1
|
||||
CATEGORIES= math
|
||||
HOMEPAGE= http://coq.inria.fr/
|
||||
|
||||
@ -13,12 +13,23 @@ PERMIT_PACKAGE_FTP= Yes
|
||||
PERMIT_DISTFILES_CDROM= Yes
|
||||
PERMIT_DISTFILES_FTP= Yes
|
||||
|
||||
MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V7.0/
|
||||
MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V7.3.1/
|
||||
MASTER_SITES0= ${MASTER_SITES:S@$@doc/@}
|
||||
MASTER_SITES1= http://coq.inria.fr/
|
||||
MASTER_SITES2= http://coq.inria.fr/ps/
|
||||
DISTFILES= ${DISTNAME}.tar.gz \
|
||||
doc-html.tar.gz:0 \
|
||||
all-ps-docs.tar.gz:0
|
||||
Changes.html:0 \
|
||||
Reference-Manual-all.ps.gz:0 \
|
||||
library.tar.gz:1 \
|
||||
RecTutorial.v.ps:2
|
||||
|
||||
IGNOREFILES= doc-html.tar.gz
|
||||
|
||||
DIST_SUBDIR= coq
|
||||
EXTRACT_ONLY= ${DISTNAME}.tar.gz \
|
||||
doc-html.tar.gz \
|
||||
library.tar.gz \
|
||||
|
||||
BUILD_DEPENDS= ::lang/ocaml
|
||||
|
||||
@ -27,22 +38,29 @@ FAKE_FLAGS= COQINSTALLPREFIX=${WRKINST}
|
||||
USE_GMAKE= Yes
|
||||
|
||||
CONFIGURE_STYLE= simple
|
||||
## add -opt option if there is ocamlc.opt.
|
||||
## ## add -opt option if there is ocamlc.opt.
|
||||
## CONFIGURE_ARGS= -prefix ${PREFIX} \
|
||||
## -emacslib ${PREFIX}/share/emacs/site-lisp ## -opt
|
||||
## -byteonly for architectures without Ocaml native-code compiler.
|
||||
CONFIGURE_ARGS= -prefix ${PREFIX} \
|
||||
-emacslib ${PREFIX}/share/emacs/site-lisp ## -opt
|
||||
-emacslib ${PREFIX}/share/emacs/site-lisp -byteonly
|
||||
|
||||
ALL_TARGET= world
|
||||
REGRESS_TARGET= check
|
||||
|
||||
COQ_DOCPSFILES= Changes.ps Library.ps Tutorial.ps \
|
||||
Reference-Manual-addendum.ps Reference-Manual-base.ps
|
||||
COQ_DOCHTMLFILES= Changes.html
|
||||
COQ_DOCPSFILES= RecTutorial.v.ps Reference-Manual-all.ps.gz
|
||||
|
||||
post-install:
|
||||
@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/html
|
||||
@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/html/library
|
||||
@${INSTALL_DATA} ${WRKDIR}/coq-docs-html/* ${PREFIX}/share/doc/coq/html
|
||||
@${INSTALL_DATA} ${WRKDIR}/library/* ${PREFIX}/share/doc/coq/html/library
|
||||
@for ff in ${COQ_DOCHTMLFILES} ; do \
|
||||
${INSTALL_DATA} ${FULLDISTDIR}/$${ff} ${PREFIX}/share/doc/coq/html ; \
|
||||
done
|
||||
@${INSTALL_DATA_DIR} ${PREFIX}/share/doc/coq/ps
|
||||
@for ff in ${COQ_DOCPSFILES} ; do \
|
||||
${INSTALL_DATA} ${WRKDIR}/$${ff} ${PREFIX}/share/doc/coq/ps ; \
|
||||
${INSTALL_DATA} ${FULLDISTDIR}/$${ff} ${PREFIX}/share/doc/coq/ps ; \
|
||||
done
|
||||
@strip ${PREFIX}/bin/*
|
||||
|
||||
.include <bsd.port.mk>
|
||||
|
||||
@ -1,9 +1,16 @@
|
||||
MD5 (coq/all-ps-docs.tar.gz) = 1bdcea2bf45707c8d542c5cdcd2dbbf6
|
||||
MD5 (coq/coq-7.0.tar.gz) = d0ac03af950acd27b3313043e5aa3587
|
||||
MD5 (coq/doc-html.tar.gz) = 802b110114e54068b502f37c8156cdf2
|
||||
RMD160 (coq/all-ps-docs.tar.gz) = c3aa484984949eaf0fd5aa5c1e7087aee6900dad
|
||||
RMD160 (coq/coq-7.0.tar.gz) = d3139881574f83935292e71014d1c54c260c1787
|
||||
RMD160 (coq/doc-html.tar.gz) = 75df7f07af08c97c0cb4286ccfb03d656e3d3c08
|
||||
SHA1 (coq/all-ps-docs.tar.gz) = 693187982509dec281d9d9cd028d78e812d30cf2
|
||||
SHA1 (coq/coq-7.0.tar.gz) = e550d2cc92df0813c2f16c151ab3eae6c2c6acb6
|
||||
SHA1 (coq/doc-html.tar.gz) = 3cfbcc6756cc9b30451cef07094a3c1f8a2cb7bf
|
||||
MD5 (coq/Changes.html) = fa6889dabdc877e3dcf555ce1538ce0d
|
||||
MD5 (coq/RecTutorial.v.ps) = b0e3f68fa326e64cac569f9b0da098a1
|
||||
MD5 (coq/Reference-Manual-all.ps.gz) = eb979cd0bdb66956e9e1aa565841c6c2
|
||||
MD5 (coq/coq-7.3.1.tar.gz) = bb403460bb51de80605b79dfa04fe807
|
||||
MD5 (coq/doc-html.tar.gz) = IGNORE
|
||||
MD5 (coq/library.tar.gz) = df44edc0178c643e0f7f9e5f8b4acb44
|
||||
RMD160 (coq/Changes.html) = 8d0dd1e9957673efbe3a1638f8d7626d840cc792
|
||||
RMD160 (coq/RecTutorial.v.ps) = bcc8967bfcf2df0e4b3671a2918189ed68bda225
|
||||
RMD160 (coq/Reference-Manual-all.ps.gz) = fcdabfbe91d4a01a5b42a7d02817e74759f702e6
|
||||
RMD160 (coq/coq-7.3.1.tar.gz) = a104a378e27fe605abe302508f12942e9460cc2f
|
||||
RMD160 (coq/library.tar.gz) = f1e9ad855c27bb1a5045867df9ba1b56553470ed
|
||||
SHA1 (coq/Changes.html) = fe3e38b12a6cae141de27c46e9e1cb16999c90fa
|
||||
SHA1 (coq/RecTutorial.v.ps) = 18f4d022aa0065bab3506f9a79e626d6a8cacfd4
|
||||
SHA1 (coq/Reference-Manual-all.ps.gz) = 17bd9cb9fba01578dea7c02fc2bec07680a12c7c
|
||||
SHA1 (coq/coq-7.3.1.tar.gz) = 85627e5ae31f80a9f7b1dfd8d2573bfd4ebe2871
|
||||
SHA1 (coq/library.tar.gz) = 8dcbc596bbcdb3186cc24f5999c43872226eca4c
|
||||
|
||||
11
math/coq/patches/patch-configure
Normal file
11
math/coq/patches/patch-configure
Normal file
@ -0,0 +1,11 @@
|
||||
--- configure.orig Thu Oct 3 14:46:22 2002
|
||||
+++ configure Mon Nov 4 13:12:09 2002
|
||||
@@ -402,7 +402,7 @@ PRINTF=`which printf`
|
||||
|
||||
# Subdirectories of theories/ added in coq_config.ml
|
||||
subdirs () {
|
||||
- (cd $1; find . -type d ! -name CVS ! -regex ".*extraction/test.*" ! -name . -exec $PRINTF "\"%s\";\n" {} \; >> $mlconfig_file)
|
||||
+ (cd $1; find . -type d ! -name CVS ! -path "*extraction/test*" ! -name . -exec $PRINTF "\"%s\";\n" {} \; >> $mlconfig_file)
|
||||
}
|
||||
|
||||
echo "let theories_dirs = [" >> $mlconfig_file
|
||||
@ -1,13 +1,13 @@
|
||||
@comment $OpenBSD: PLIST,v 1.1.1.1 2001/09/22 14:24:31 naddy Exp $
|
||||
@comment $OpenBSD: PLIST,v 1.2 2002/11/04 21:10:44 naddy Exp $
|
||||
bin/coq-interface
|
||||
bin/coq-tex
|
||||
bin/coq_makefile
|
||||
bin/coq_vo2xml
|
||||
bin/coqc
|
||||
bin/coqdep
|
||||
bin/coqmktop
|
||||
bin/coqtop
|
||||
bin/coqtop.byte
|
||||
bin/coqtop.opt
|
||||
bin/gallina
|
||||
bin/parser
|
||||
lib/coq/contrib/correctness/ArrayPermut.vo
|
||||
@ -28,18 +28,21 @@ lib/coq/contrib/fourier/Fourier.vo
|
||||
lib/coq/contrib/fourier/Fourier_util.vo
|
||||
lib/coq/contrib/interface/Centaur.vo
|
||||
lib/coq/contrib/interface/vernacrc
|
||||
lib/coq/contrib/jprover/JProver.vo
|
||||
lib/coq/contrib/omega/Omega.vo
|
||||
lib/coq/contrib/omega/OmegaSyntax.vo
|
||||
lib/coq/contrib/omega/Zcomplements.vo
|
||||
lib/coq/contrib/omega/Zlogarithm.vo
|
||||
lib/coq/contrib/omega/Zpower.vo
|
||||
lib/coq/contrib/ring/ArithRing.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/contrib/xml/Xml.vo
|
||||
lib/coq/states/barestate.coq
|
||||
lib/coq/states/initial.coq
|
||||
@ -49,6 +52,7 @@ lib/coq/tactics/EqDecide.vo
|
||||
lib/coq/tactics/Equality.vo
|
||||
lib/coq/tactics/Inv.vo
|
||||
lib/coq/tactics/Refine.vo
|
||||
lib/coq/tactics/Setoid_replace.vo
|
||||
lib/coq/tactics/Tauto.vo
|
||||
lib/coq/theories/Arith/Arith.vo
|
||||
lib/coq/theories/Arith/Between.vo
|
||||
@ -61,6 +65,7 @@ lib/coq/theories/Arith/Even.vo
|
||||
lib/coq/theories/Arith/Gt.vo
|
||||
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/Minus.vo
|
||||
lib/coq/theories/Arith/Mult.vo
|
||||
@ -106,6 +111,7 @@ lib/coq/theories/Lists/PolyList.vo
|
||||
lib/coq/theories/Lists/PolyListSyntax.vo
|
||||
lib/coq/theories/Lists/Streams.vo
|
||||
lib/coq/theories/Lists/TheoryList.vo
|
||||
lib/coq/theories/Logic/Berardi.vo
|
||||
lib/coq/theories/Logic/Classical.vo
|
||||
lib/coq/theories/Logic/Classical_Pred_Set.vo
|
||||
lib/coq/theories/Logic/Classical_Pred_Type.vo
|
||||
@ -117,6 +123,8 @@ lib/coq/theories/Logic/Eqdep_dec.vo
|
||||
lib/coq/theories/Logic/JMeq.vo
|
||||
lib/coq/theories/Reals/DiscrR.vo
|
||||
lib/coq/theories/Reals/R_Ifp.vo
|
||||
lib/coq/theories/Reals/R_sqr.vo
|
||||
lib/coq/theories/Reals/Ranalysis.vo
|
||||
lib/coq/theories/Reals/Raxioms.vo
|
||||
lib/coq/theories/Reals/Rbase.vo
|
||||
lib/coq/theories/Reals/Rbasic_fun.vo
|
||||
@ -124,9 +132,12 @@ lib/coq/theories/Reals/Rdefinitions.vo
|
||||
lib/coq/theories/Reals/Rderiv.vo
|
||||
lib/coq/theories/Reals/Reals.vo
|
||||
lib/coq/theories/Reals/Rfunctions.vo
|
||||
lib/coq/theories/Reals/Rgeom.vo
|
||||
lib/coq/theories/Reals/Rlimit.vo
|
||||
lib/coq/theories/Reals/Rseries.vo
|
||||
lib/coq/theories/Reals/Rsigma.vo
|
||||
lib/coq/theories/Reals/Rsyntax.vo
|
||||
lib/coq/theories/Reals/Rtrigo.vo
|
||||
lib/coq/theories/Reals/Rtrigo_fun.vo
|
||||
lib/coq/theories/Reals/SplitAbsolu.vo
|
||||
lib/coq/theories/Reals/SplitRmult.vo
|
||||
@ -137,6 +148,7 @@ 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
|
||||
lib/coq/theories/Sets/Cpo.vo
|
||||
@ -159,6 +171,9 @@ lib/coq/theories/Sets/Relations_2_facts.vo
|
||||
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/Permutation.vo
|
||||
lib/coq/theories/Sorting/Sorting.vo
|
||||
lib/coq/theories/Wellfounded/Disjoint_Union.vo
|
||||
lib/coq/theories/Wellfounded/Inclusion.vo
|
||||
lib/coq/theories/Wellfounded/Inverse_Image.vo
|
||||
@ -171,7 +186,12 @@ lib/coq/theories/Wellfounded/Wellfounded.vo
|
||||
lib/coq/theories/ZArith/Wf_Z.vo
|
||||
lib/coq/theories/ZArith/ZArith.vo
|
||||
lib/coq/theories/ZArith/ZArith_dec.vo
|
||||
lib/coq/theories/ZArith/Zcomplements.vo
|
||||
lib/coq/theories/ZArith/Zdiv.vo
|
||||
lib/coq/theories/ZArith/Zhints.vo
|
||||
lib/coq/theories/ZArith/Zlogarithm.vo
|
||||
lib/coq/theories/ZArith/Zmisc.vo
|
||||
lib/coq/theories/ZArith/Zpower.vo
|
||||
lib/coq/theories/ZArith/Zsyntax.vo
|
||||
lib/coq/theories/ZArith/auxiliary.vo
|
||||
lib/coq/theories/ZArith/fast_integer.vo
|
||||
@ -179,6 +199,7 @@ lib/coq/theories/ZArith/zarith_aux.vo
|
||||
man/man1/coq-interface.1
|
||||
man/man1/coq-tex.1
|
||||
man/man1/coq_makefile.1
|
||||
man/man1/coq_vo2xml.1
|
||||
man/man1/coqc.1
|
||||
man/man1/coqdep.1
|
||||
man/man1/coqmktop.1
|
||||
@ -187,9 +208,392 @@ man/man1/coqtop.byte.1
|
||||
man/man1/coqtop.opt.1
|
||||
man/man1/gallina.1
|
||||
man/man1/parser.1
|
||||
share/doc/coq/html/Library.html
|
||||
share/doc/coq/html/changes.html
|
||||
share/doc/coq/html/Changes.html
|
||||
share/doc/coq/html/cover.html
|
||||
share/doc/coq/html/library/Coq.Arith.Arith.html
|
||||
share/doc/coq/html/library/Coq.Arith.Between.html
|
||||
share/doc/coq/html/library/Coq.Arith.Compare.html
|
||||
share/doc/coq/html/library/Coq.Arith.Compare_dec.html
|
||||
share/doc/coq/html/library/Coq.Arith.Div.html
|
||||
share/doc/coq/html/library/Coq.Arith.Div2.html
|
||||
share/doc/coq/html/library/Coq.Arith.EqNat.html
|
||||
share/doc/coq/html/library/Coq.Arith.Euclid.html
|
||||
share/doc/coq/html/library/Coq.Arith.Even.html
|
||||
share/doc/coq/html/library/Coq.Arith.Gt.html
|
||||
share/doc/coq/html/library/Coq.Arith.Le.html
|
||||
share/doc/coq/html/library/Coq.Arith.Lt.html
|
||||
share/doc/coq/html/library/Coq.Arith.Max.html
|
||||
share/doc/coq/html/library/Coq.Arith.Min.html
|
||||
share/doc/coq/html/library/Coq.Arith.Minus.html
|
||||
share/doc/coq/html/library/Coq.Arith.Mult.html
|
||||
share/doc/coq/html/library/Coq.Arith.Peano_dec.html
|
||||
share/doc/coq/html/library/Coq.Arith.Plus.html
|
||||
share/doc/coq/html/library/Coq.Arith.Wf_nat.html
|
||||
share/doc/coq/html/library/Coq.Bool.Bool.html
|
||||
share/doc/coq/html/library/Coq.Bool.BoolEq.html
|
||||
share/doc/coq/html/library/Coq.Bool.DecBool.html
|
||||
share/doc/coq/html/library/Coq.Bool.IfProp.html
|
||||
share/doc/coq/html/library/Coq.Bool.Sumbool.html
|
||||
share/doc/coq/html/library/Coq.Bool.Zerob.html
|
||||
share/doc/coq/html/library/Coq.Init.Datatypes.html
|
||||
share/doc/coq/html/library/Coq.Init.DatatypesSyntax.html
|
||||
share/doc/coq/html/library/Coq.Init.Logic.html
|
||||
share/doc/coq/html/library/Coq.Init.LogicSyntax.html
|
||||
share/doc/coq/html/library/Coq.Init.Logic_Type.html
|
||||
share/doc/coq/html/library/Coq.Init.Logic_TypeSyntax.html
|
||||
share/doc/coq/html/library/Coq.Init.Peano.html
|
||||
share/doc/coq/html/library/Coq.Init.Prelude.html
|
||||
share/doc/coq/html/library/Coq.Init.Specif.html
|
||||
share/doc/coq/html/library/Coq.Init.SpecifSyntax.html
|
||||
share/doc/coq/html/library/Coq.Init.Wf.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Adalloc.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Addec.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Addr.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Adist.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Allmaps.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Fset.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Lsort.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Map.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapaxioms.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapc.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapcanon.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapcard.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapfold.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapiter.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Maplists.html
|
||||
share/doc/coq/html/library/Coq.IntMap.Mapsubset.html
|
||||
share/doc/coq/html/library/Coq.Lists.List.html
|
||||
share/doc/coq/html/library/Coq.Lists.ListSet.html
|
||||
share/doc/coq/html/library/Coq.Lists.PolyList.html
|
||||
share/doc/coq/html/library/Coq.Lists.PolyListSyntax.html
|
||||
share/doc/coq/html/library/Coq.Lists.Streams.html
|
||||
share/doc/coq/html/library/Coq.Lists.TheoryList.html
|
||||
share/doc/coq/html/library/Coq.Logic.Berardi.html
|
||||
share/doc/coq/html/library/Coq.Logic.Classical.html
|
||||
share/doc/coq/html/library/Coq.Logic.Classical_Pred_Set.html
|
||||
share/doc/coq/html/library/Coq.Logic.Classical_Pred_Type.html
|
||||
share/doc/coq/html/library/Coq.Logic.Classical_Prop.html
|
||||
share/doc/coq/html/library/Coq.Logic.Classical_Type.html
|
||||
share/doc/coq/html/library/Coq.Logic.Decidable.html
|
||||
share/doc/coq/html/library/Coq.Logic.Elimdep.html
|
||||
share/doc/coq/html/library/Coq.Logic.Eqdep.html
|
||||
share/doc/coq/html/library/Coq.Logic.Eqdep_dec.html
|
||||
share/doc/coq/html/library/Coq.Logic.JMeq.html
|
||||
share/doc/coq/html/library/Coq.Num.AddProps.html
|
||||
share/doc/coq/html/library/Coq.Num.Axioms.html
|
||||
share/doc/coq/html/library/Coq.Num.Definitions.html
|
||||
share/doc/coq/html/library/Coq.Num.DiscrAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.DiscrProps.html
|
||||
share/doc/coq/html/library/Coq.Num.EqAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.EqParams.html
|
||||
share/doc/coq/html/library/Coq.Num.GeAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.GeProps.html
|
||||
share/doc/coq/html/library/Coq.Num.GtAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.GtProps.html
|
||||
share/doc/coq/html/library/Coq.Num.LeAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.LeProps.html
|
||||
share/doc/coq/html/library/Coq.Num.LtProps.html
|
||||
share/doc/coq/html/library/Coq.Num.NSyntax.html
|
||||
share/doc/coq/html/library/Coq.Num.NeqAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.NeqDef.html
|
||||
share/doc/coq/html/library/Coq.Num.NeqParams.html
|
||||
share/doc/coq/html/library/Coq.Num.NeqProps.html
|
||||
share/doc/coq/html/library/Coq.Num.OppAxioms.html
|
||||
share/doc/coq/html/library/Coq.Num.OppProps.html
|
||||
share/doc/coq/html/library/Coq.Num.Params.html
|
||||
share/doc/coq/html/library/Coq.Num.SubProps.html
|
||||
share/doc/coq/html/library/Coq.Reals.DiscrR.html
|
||||
share/doc/coq/html/library/Coq.Reals.R_Ifp.html
|
||||
share/doc/coq/html/library/Coq.Reals.R_sqr.html
|
||||
share/doc/coq/html/library/Coq.Reals.Ranalysis.html
|
||||
share/doc/coq/html/library/Coq.Reals.Raxioms.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rbase.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rbasic_fun.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rdefinitions.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rderiv.html
|
||||
share/doc/coq/html/library/Coq.Reals.Reals.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rfunctions.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rgeom.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rlimit.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rseries.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rsigma.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rsyntax.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rtrigo.html
|
||||
share/doc/coq/html/library/Coq.Reals.Rtrigo_fun.html
|
||||
share/doc/coq/html/library/Coq.Reals.SplitAbsolu.html
|
||||
share/doc/coq/html/library/Coq.Reals.SplitRmult.html
|
||||
share/doc/coq/html/library/Coq.Reals.TypeSyntax.html
|
||||
share/doc/coq/html/library/Coq.Relations.Newman.html
|
||||
share/doc/coq/html/library/Coq.Relations.Operators_Properties.html
|
||||
share/doc/coq/html/library/Coq.Relations.Relation_Definitions.html
|
||||
share/doc/coq/html/library/Coq.Relations.Relation_Operators.html
|
||||
share/doc/coq/html/library/Coq.Relations.Relations.html
|
||||
share/doc/coq/html/library/Coq.Relations.Rstar.html
|
||||
share/doc/coq/html/library/Coq.Setoids.Setoid.html
|
||||
share/doc/coq/html/library/Coq.Sets.Classical_sets.html
|
||||
share/doc/coq/html/library/Coq.Sets.Constructive_sets.html
|
||||
share/doc/coq/html/library/Coq.Sets.Cpo.html
|
||||
share/doc/coq/html/library/Coq.Sets.Ensembles.html
|
||||
share/doc/coq/html/library/Coq.Sets.Finite_sets.html
|
||||
share/doc/coq/html/library/Coq.Sets.Finite_sets_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Image.html
|
||||
share/doc/coq/html/library/Coq.Sets.Infinite_sets.html
|
||||
share/doc/coq/html/library/Coq.Sets.Integers.html
|
||||
share/doc/coq/html/library/Coq.Sets.Multiset.html
|
||||
share/doc/coq/html/library/Coq.Sets.Partial_Order.html
|
||||
share/doc/coq/html/library/Coq.Sets.Permut.html
|
||||
share/doc/coq/html/library/Coq.Sets.Powerset.html
|
||||
share/doc/coq/html/library/Coq.Sets.Powerset_Classical_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Powerset_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_1.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_1_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_2.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_2_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_3.html
|
||||
share/doc/coq/html/library/Coq.Sets.Relations_3_facts.html
|
||||
share/doc/coq/html/library/Coq.Sets.Uniset.html
|
||||
share/doc/coq/html/library/Coq.Sorting.Heap.html
|
||||
share/doc/coq/html/library/Coq.Sorting.Permutation.html
|
||||
share/doc/coq/html/library/Coq.Sorting.Sorting.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Disjoint_Union.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Inclusion.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Inverse_Image.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Lexicographic_Exponentiation.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Lexicographic_Product.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Transitive_Closure.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Union.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Well_Ordering.html
|
||||
share/doc/coq/html/library/Coq.Wellfounded.Wellfounded.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Wf_Z.html
|
||||
share/doc/coq/html/library/Coq.ZArith.ZArith.html
|
||||
share/doc/coq/html/library/Coq.ZArith.ZArith_dec.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zcomplements.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zhints.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zlogarithm.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zmisc.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zpower.html
|
||||
share/doc/coq/html/library/Coq.ZArith.Zsyntax.html
|
||||
share/doc/coq/html/library/Coq.ZArith.auxiliary.html
|
||||
share/doc/coq/html/library/Coq.ZArith.fast_integer.html
|
||||
share/doc/coq/html/library/Coq.ZArith.zarith_aux.html
|
||||
share/doc/coq/html/library/index.html
|
||||
share/doc/coq/html/library/index_axiom_A.html
|
||||
share/doc/coq/html/library/index_axiom_B.html
|
||||
share/doc/coq/html/library/index_axiom_C.html
|
||||
share/doc/coq/html/library/index_axiom_D.html
|
||||
share/doc/coq/html/library/index_axiom_E.html
|
||||
share/doc/coq/html/library/index_axiom_F.html
|
||||
share/doc/coq/html/library/index_axiom_G.html
|
||||
share/doc/coq/html/library/index_axiom_H.html
|
||||
share/doc/coq/html/library/index_axiom_I.html
|
||||
share/doc/coq/html/library/index_axiom_J.html
|
||||
share/doc/coq/html/library/index_axiom_K.html
|
||||
share/doc/coq/html/library/index_axiom_L.html
|
||||
share/doc/coq/html/library/index_axiom_M.html
|
||||
share/doc/coq/html/library/index_axiom_N.html
|
||||
share/doc/coq/html/library/index_axiom_O.html
|
||||
share/doc/coq/html/library/index_axiom_P.html
|
||||
share/doc/coq/html/library/index_axiom_Q.html
|
||||
share/doc/coq/html/library/index_axiom_R.html
|
||||
share/doc/coq/html/library/index_axiom_S.html
|
||||
share/doc/coq/html/library/index_axiom_T.html
|
||||
share/doc/coq/html/library/index_axiom_U.html
|
||||
share/doc/coq/html/library/index_axiom_V.html
|
||||
share/doc/coq/html/library/index_axiom_W.html
|
||||
share/doc/coq/html/library/index_axiom_X.html
|
||||
share/doc/coq/html/library/index_axiom_Y.html
|
||||
share/doc/coq/html/library/index_axiom_Z.html
|
||||
share/doc/coq/html/library/index_axiom__.html
|
||||
share/doc/coq/html/library/index_constructor_A.html
|
||||
share/doc/coq/html/library/index_constructor_B.html
|
||||
share/doc/coq/html/library/index_constructor_C.html
|
||||
share/doc/coq/html/library/index_constructor_D.html
|
||||
share/doc/coq/html/library/index_constructor_E.html
|
||||
share/doc/coq/html/library/index_constructor_F.html
|
||||
share/doc/coq/html/library/index_constructor_G.html
|
||||
share/doc/coq/html/library/index_constructor_H.html
|
||||
share/doc/coq/html/library/index_constructor_I.html
|
||||
share/doc/coq/html/library/index_constructor_J.html
|
||||
share/doc/coq/html/library/index_constructor_K.html
|
||||
share/doc/coq/html/library/index_constructor_L.html
|
||||
share/doc/coq/html/library/index_constructor_M.html
|
||||
share/doc/coq/html/library/index_constructor_N.html
|
||||
share/doc/coq/html/library/index_constructor_O.html
|
||||
share/doc/coq/html/library/index_constructor_P.html
|
||||
share/doc/coq/html/library/index_constructor_Q.html
|
||||
share/doc/coq/html/library/index_constructor_R.html
|
||||
share/doc/coq/html/library/index_constructor_S.html
|
||||
share/doc/coq/html/library/index_constructor_T.html
|
||||
share/doc/coq/html/library/index_constructor_U.html
|
||||
share/doc/coq/html/library/index_constructor_V.html
|
||||
share/doc/coq/html/library/index_constructor_W.html
|
||||
share/doc/coq/html/library/index_constructor_X.html
|
||||
share/doc/coq/html/library/index_constructor_Y.html
|
||||
share/doc/coq/html/library/index_constructor_Z.html
|
||||
share/doc/coq/html/library/index_constructor__.html
|
||||
share/doc/coq/html/library/index_definition_A.html
|
||||
share/doc/coq/html/library/index_definition_B.html
|
||||
share/doc/coq/html/library/index_definition_C.html
|
||||
share/doc/coq/html/library/index_definition_D.html
|
||||
share/doc/coq/html/library/index_definition_E.html
|
||||
share/doc/coq/html/library/index_definition_F.html
|
||||
share/doc/coq/html/library/index_definition_G.html
|
||||
share/doc/coq/html/library/index_definition_H.html
|
||||
share/doc/coq/html/library/index_definition_I.html
|
||||
share/doc/coq/html/library/index_definition_J.html
|
||||
share/doc/coq/html/library/index_definition_K.html
|
||||
share/doc/coq/html/library/index_definition_L.html
|
||||
share/doc/coq/html/library/index_definition_M.html
|
||||
share/doc/coq/html/library/index_definition_N.html
|
||||
share/doc/coq/html/library/index_definition_O.html
|
||||
share/doc/coq/html/library/index_definition_P.html
|
||||
share/doc/coq/html/library/index_definition_Q.html
|
||||
share/doc/coq/html/library/index_definition_R.html
|
||||
share/doc/coq/html/library/index_definition_S.html
|
||||
share/doc/coq/html/library/index_definition_T.html
|
||||
share/doc/coq/html/library/index_definition_U.html
|
||||
share/doc/coq/html/library/index_definition_V.html
|
||||
share/doc/coq/html/library/index_definition_W.html
|
||||
share/doc/coq/html/library/index_definition_X.html
|
||||
share/doc/coq/html/library/index_definition_Y.html
|
||||
share/doc/coq/html/library/index_definition_Z.html
|
||||
share/doc/coq/html/library/index_definition__.html
|
||||
share/doc/coq/html/library/index_global_A.html
|
||||
share/doc/coq/html/library/index_global_B.html
|
||||
share/doc/coq/html/library/index_global_C.html
|
||||
share/doc/coq/html/library/index_global_D.html
|
||||
share/doc/coq/html/library/index_global_E.html
|
||||
share/doc/coq/html/library/index_global_F.html
|
||||
share/doc/coq/html/library/index_global_G.html
|
||||
share/doc/coq/html/library/index_global_H.html
|
||||
share/doc/coq/html/library/index_global_I.html
|
||||
share/doc/coq/html/library/index_global_J.html
|
||||
share/doc/coq/html/library/index_global_K.html
|
||||
share/doc/coq/html/library/index_global_L.html
|
||||
share/doc/coq/html/library/index_global_M.html
|
||||
share/doc/coq/html/library/index_global_N.html
|
||||
share/doc/coq/html/library/index_global_O.html
|
||||
share/doc/coq/html/library/index_global_P.html
|
||||
share/doc/coq/html/library/index_global_Q.html
|
||||
share/doc/coq/html/library/index_global_R.html
|
||||
share/doc/coq/html/library/index_global_S.html
|
||||
share/doc/coq/html/library/index_global_T.html
|
||||
share/doc/coq/html/library/index_global_U.html
|
||||
share/doc/coq/html/library/index_global_V.html
|
||||
share/doc/coq/html/library/index_global_W.html
|
||||
share/doc/coq/html/library/index_global_X.html
|
||||
share/doc/coq/html/library/index_global_Y.html
|
||||
share/doc/coq/html/library/index_global_Z.html
|
||||
share/doc/coq/html/library/index_global__.html
|
||||
share/doc/coq/html/library/index_inductive_A.html
|
||||
share/doc/coq/html/library/index_inductive_B.html
|
||||
share/doc/coq/html/library/index_inductive_C.html
|
||||
share/doc/coq/html/library/index_inductive_D.html
|
||||
share/doc/coq/html/library/index_inductive_E.html
|
||||
share/doc/coq/html/library/index_inductive_F.html
|
||||
share/doc/coq/html/library/index_inductive_G.html
|
||||
share/doc/coq/html/library/index_inductive_H.html
|
||||
share/doc/coq/html/library/index_inductive_I.html
|
||||
share/doc/coq/html/library/index_inductive_J.html
|
||||
share/doc/coq/html/library/index_inductive_K.html
|
||||
share/doc/coq/html/library/index_inductive_L.html
|
||||
share/doc/coq/html/library/index_inductive_M.html
|
||||
share/doc/coq/html/library/index_inductive_N.html
|
||||
share/doc/coq/html/library/index_inductive_O.html
|
||||
share/doc/coq/html/library/index_inductive_P.html
|
||||
share/doc/coq/html/library/index_inductive_Q.html
|
||||
share/doc/coq/html/library/index_inductive_R.html
|
||||
share/doc/coq/html/library/index_inductive_S.html
|
||||
share/doc/coq/html/library/index_inductive_T.html
|
||||
share/doc/coq/html/library/index_inductive_U.html
|
||||
share/doc/coq/html/library/index_inductive_V.html
|
||||
share/doc/coq/html/library/index_inductive_W.html
|
||||
share/doc/coq/html/library/index_inductive_X.html
|
||||
share/doc/coq/html/library/index_inductive_Y.html
|
||||
share/doc/coq/html/library/index_inductive_Z.html
|
||||
share/doc/coq/html/library/index_inductive__.html
|
||||
share/doc/coq/html/library/index_lemma_A.html
|
||||
share/doc/coq/html/library/index_lemma_B.html
|
||||
share/doc/coq/html/library/index_lemma_C.html
|
||||
share/doc/coq/html/library/index_lemma_D.html
|
||||
share/doc/coq/html/library/index_lemma_E.html
|
||||
share/doc/coq/html/library/index_lemma_F.html
|
||||
share/doc/coq/html/library/index_lemma_G.html
|
||||
share/doc/coq/html/library/index_lemma_H.html
|
||||
share/doc/coq/html/library/index_lemma_I.html
|
||||
share/doc/coq/html/library/index_lemma_J.html
|
||||
share/doc/coq/html/library/index_lemma_K.html
|
||||
share/doc/coq/html/library/index_lemma_L.html
|
||||
share/doc/coq/html/library/index_lemma_M.html
|
||||
share/doc/coq/html/library/index_lemma_N.html
|
||||
share/doc/coq/html/library/index_lemma_O.html
|
||||
share/doc/coq/html/library/index_lemma_P.html
|
||||
share/doc/coq/html/library/index_lemma_Q.html
|
||||
share/doc/coq/html/library/index_lemma_R.html
|
||||
share/doc/coq/html/library/index_lemma_S.html
|
||||
share/doc/coq/html/library/index_lemma_T.html
|
||||
share/doc/coq/html/library/index_lemma_U.html
|
||||
share/doc/coq/html/library/index_lemma_V.html
|
||||
share/doc/coq/html/library/index_lemma_W.html
|
||||
share/doc/coq/html/library/index_lemma_X.html
|
||||
share/doc/coq/html/library/index_lemma_Y.html
|
||||
share/doc/coq/html/library/index_lemma_Z.html
|
||||
share/doc/coq/html/library/index_lemma__.html
|
||||
share/doc/coq/html/library/index_module_A.html
|
||||
share/doc/coq/html/library/index_module_B.html
|
||||
share/doc/coq/html/library/index_module_C.html
|
||||
share/doc/coq/html/library/index_module_D.html
|
||||
share/doc/coq/html/library/index_module_E.html
|
||||
share/doc/coq/html/library/index_module_F.html
|
||||
share/doc/coq/html/library/index_module_G.html
|
||||
share/doc/coq/html/library/index_module_H.html
|
||||
share/doc/coq/html/library/index_module_I.html
|
||||
share/doc/coq/html/library/index_module_J.html
|
||||
share/doc/coq/html/library/index_module_K.html
|
||||
share/doc/coq/html/library/index_module_L.html
|
||||
share/doc/coq/html/library/index_module_M.html
|
||||
share/doc/coq/html/library/index_module_N.html
|
||||
share/doc/coq/html/library/index_module_O.html
|
||||
share/doc/coq/html/library/index_module_P.html
|
||||
share/doc/coq/html/library/index_module_Q.html
|
||||
share/doc/coq/html/library/index_module_R.html
|
||||
share/doc/coq/html/library/index_module_S.html
|
||||
share/doc/coq/html/library/index_module_T.html
|
||||
share/doc/coq/html/library/index_module_U.html
|
||||
share/doc/coq/html/library/index_module_V.html
|
||||
share/doc/coq/html/library/index_module_W.html
|
||||
share/doc/coq/html/library/index_module_X.html
|
||||
share/doc/coq/html/library/index_module_Y.html
|
||||
share/doc/coq/html/library/index_module_Z.html
|
||||
share/doc/coq/html/library/index_module__.html
|
||||
share/doc/coq/html/library/index_tactic_A.html
|
||||
share/doc/coq/html/library/index_tactic_B.html
|
||||
share/doc/coq/html/library/index_tactic_C.html
|
||||
share/doc/coq/html/library/index_tactic_D.html
|
||||
share/doc/coq/html/library/index_tactic_E.html
|
||||
share/doc/coq/html/library/index_tactic_F.html
|
||||
share/doc/coq/html/library/index_tactic_G.html
|
||||
share/doc/coq/html/library/index_tactic_H.html
|
||||
share/doc/coq/html/library/index_tactic_I.html
|
||||
share/doc/coq/html/library/index_tactic_J.html
|
||||
share/doc/coq/html/library/index_tactic_K.html
|
||||
share/doc/coq/html/library/index_tactic_L.html
|
||||
share/doc/coq/html/library/index_tactic_M.html
|
||||
share/doc/coq/html/library/index_tactic_N.html
|
||||
share/doc/coq/html/library/index_tactic_O.html
|
||||
share/doc/coq/html/library/index_tactic_P.html
|
||||
share/doc/coq/html/library/index_tactic_Q.html
|
||||
share/doc/coq/html/library/index_tactic_R.html
|
||||
share/doc/coq/html/library/index_tactic_S.html
|
||||
share/doc/coq/html/library/index_tactic_T.html
|
||||
share/doc/coq/html/library/index_tactic_U.html
|
||||
share/doc/coq/html/library/index_tactic_V.html
|
||||
share/doc/coq/html/library/index_tactic_W.html
|
||||
share/doc/coq/html/library/index_tactic_X.html
|
||||
share/doc/coq/html/library/index_tactic_Y.html
|
||||
share/doc/coq/html/library/index_tactic_Z.html
|
||||
share/doc/coq/html/library/index_tactic__.html
|
||||
share/doc/coq/html/library/style.css
|
||||
share/doc/coq/html/main-0.html
|
||||
share/doc/coq/html/main.html
|
||||
share/doc/coq/html/next.gif
|
||||
@ -204,6 +608,7 @@ share/doc/coq/html/node.0.1.3.html
|
||||
share/doc/coq/html/node.0.1.4.html
|
||||
share/doc/coq/html/node.0.1.5.html
|
||||
share/doc/coq/html/node.0.1.6.html
|
||||
share/doc/coq/html/node.0.1.7.html
|
||||
share/doc/coq/html/node.0.1.html
|
||||
share/doc/coq/html/node.0.2.0.html
|
||||
share/doc/coq/html/node.0.2.1.html
|
||||
@ -284,9 +689,12 @@ share/doc/coq/html/node.3.2.1.html
|
||||
share/doc/coq/html/node.3.2.2.html
|
||||
share/doc/coq/html/node.3.2.3.html
|
||||
share/doc/coq/html/node.3.2.4.html
|
||||
share/doc/coq/html/node.3.2.5.html
|
||||
share/doc/coq/html/node.3.2.6.html
|
||||
share/doc/coq/html/node.3.2.html
|
||||
share/doc/coq/html/node.3.3.0.html
|
||||
share/doc/coq/html/node.3.3.1.html
|
||||
share/doc/coq/html/node.3.3.10.html
|
||||
share/doc/coq/html/node.3.3.2.html
|
||||
share/doc/coq/html/node.3.3.3.html
|
||||
share/doc/coq/html/node.3.3.4.html
|
||||
@ -312,6 +720,7 @@ share/doc/coq/html/node.3.5.html
|
||||
share/doc/coq/html/node.3.6.0.html
|
||||
share/doc/coq/html/node.3.6.1.html
|
||||
share/doc/coq/html/node.3.6.2.html
|
||||
share/doc/coq/html/node.3.6.3.html
|
||||
share/doc/coq/html/node.3.6.html
|
||||
share/doc/coq/html/node.3.7.0.html
|
||||
share/doc/coq/html/node.3.7.1.html
|
||||
@ -322,6 +731,11 @@ share/doc/coq/html/node.3.7.5.html
|
||||
share/doc/coq/html/node.3.7.6.html
|
||||
share/doc/coq/html/node.3.7.7.html
|
||||
share/doc/coq/html/node.3.7.html
|
||||
share/doc/coq/html/node.3.8.0.html
|
||||
share/doc/coq/html/node.3.8.1.html
|
||||
share/doc/coq/html/node.3.8.2.html
|
||||
share/doc/coq/html/node.3.8.3.html
|
||||
share/doc/coq/html/node.3.8.html
|
||||
share/doc/coq/html/node.3.html
|
||||
share/doc/coq/html/node.4.html
|
||||
share/doc/coq/html/node.5.html
|
||||
@ -341,18 +755,21 @@ share/doc/coq/html/root.gif
|
||||
share/doc/coq/html/sub.gif
|
||||
share/doc/coq/html/toc.html
|
||||
share/doc/coq/html/tutorial.html
|
||||
share/doc/coq/ps/Changes.ps
|
||||
share/doc/coq/ps/Library.ps
|
||||
share/doc/coq/ps/Reference-Manual-addendum.ps
|
||||
share/doc/coq/ps/Reference-Manual-base.ps
|
||||
share/doc/coq/ps/Tutorial.ps
|
||||
share/doc/coq/ps/RecTutorial.v.ps
|
||||
share/doc/coq/ps/Reference-Manual-all.ps.gz
|
||||
share/emacs/site-lisp/coq-inferior.el
|
||||
share/emacs/site-lisp/coq.el
|
||||
@dirrm share/emacs/site-lisp
|
||||
@dirrm share/emacs
|
||||
@dirrm share/doc/coq/ps
|
||||
@dirrm share/doc/coq/html/library
|
||||
@dirrm share/doc/coq/html
|
||||
@dirrm share/doc/coq
|
||||
@dirrm lib/coq/theories/ZArith
|
||||
@dirrm lib/coq/theories/Wellfounded
|
||||
@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/Logic
|
||||
@ -365,8 +782,10 @@ share/emacs/site-lisp/coq.el
|
||||
@dirrm lib/coq/tactics
|
||||
@dirrm lib/coq/states
|
||||
@dirrm lib/coq/contrib/xml
|
||||
@dirrm lib/coq/contrib/romega
|
||||
@dirrm lib/coq/contrib/ring
|
||||
@dirrm lib/coq/contrib/omega
|
||||
@dirrm lib/coq/contrib/jprover
|
||||
@dirrm lib/coq/contrib/interface
|
||||
@dirrm lib/coq/contrib/fourier
|
||||
@dirrm lib/coq/contrib/field
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user