Attachment #48105 for bug #73634

View | Details | Raw Unified | Return to bug 73634
Collapse All | Expand All




#

PORTNAME=	coq
PORTVERSION=	8.0p1
CATEGORIES=	math
MASTER_SITES=	ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/
DISTNAME=	coq-8.0pl1

PATCH_SITES=	${MASTER_SITES}
#only for Ocaml 3.08.1 :
PATCHFILES=	patch-coq-8.0pl1-ocaml-3.08.1

MAINTAINER=	r.c.ladan@student.tue.nl

CONFIGURE_ARGS+=	--opt

ALL_TARGET=	world
#no lablgl2 in ports yet

.include <bsd.port.pre.mk>

.if exists(${LOCALBASE}/bin/lablgtk2)
BUILD_DEPENDS+=	lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
RUN_DEPENDS+=	${BUILD_DEPENDS}
PLIST_SUB+=	IDE=""
.else
PLIST_SUB+=	IDE="@comment "
.endif

MAN1=	coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 coqdoc.1 \
	coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqwc.1 gallina.1 \
	parser.1

post-install:
.if !defined(NOPORTDOCS)

.endfor
.endif

.include <bsd.port.post.mk>

Lines 17-23 Link Here

(-)/usr/ports/math/coq/pkg-descr (-1 / +1 lines)
17	Coq is distributed under the GNU Lesser General Public Licence	17	Coq is distributed under the GNU Lesser General Public Licence
18	Version 2.1 (LGPL).	18	Version 2.1 (LGPL).
19		19
20	CoqIde is not yet available in this port.	20	CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
21		21
22	Author: Rene Ladan <r.c.ladan@student.tue.nl>	22	Author: Rene Ladan <r.c.ladan@student.tue.nl>
23	WWW: http://coq.inria.fr/	23	WWW: http://coq.inria.fr/




@comment $FreeBSD: ports/math/coq/pkg-plist,v 1.1 2004/10/16 00:55:32 pav Exp $
bin/coq-interface
bin/coq-interface.opt
bin/coq-tex

bin/coqc
bin/coqdep
bin/coqdoc
%%IDE%%bin/coqide
%%IDE%%bin/coqide.byte
%%IDE%%bin/coqide.opt
bin/coqmktop
bin/coqtop
bin/coqtop.byte

bin/parser
bin/parser.opt
lib/coq/contrib/cc/CCSolve.vo
@dirrm lib/coq/contrib/cc
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
@dirrm lib/coq/contrib/field
lib/coq/contrib/fourier/Fourier.vo
lib/coq/contrib/fourier/Fourier_util.vo
@dirrm lib/coq/contrib/fourier
lib/coq/contrib/interface/vernacrc
@dirrm lib/coq/contrib/interface
lib/coq/contrib/omega/Omega.vo
lib/coq/contrib/omega/OmegaLemmas.vo
@dirrm lib/coq/contrib/omega
lib/coq/contrib/ring/ArithRing.vo
lib/coq/contrib/ring/NArithRing.vo
lib/coq/contrib/ring/Quote.vo

lib/coq/contrib/ring/Setoid_ring_normalize.vo
lib/coq/contrib/ring/Setoid_ring_theory.vo
lib/coq/contrib/ring/ZArithRing.vo
@dirrm lib/coq/contrib/ring
lib/coq/contrib/romega/ROmega.vo
lib/coq/contrib/romega/ReflOmegaCore.vo
@dirrm lib/coq/contrib/romega
@dirrm lib/coq/contrib
lib/coq/contrib7/cc/CCSolve.vo
@dirrm lib/coq/contrib7/cc
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
@dirrm lib/coq/contrib7/field
lib/coq/contrib7/fourier/Fourier.vo
lib/coq/contrib7/fourier/Fourier_util.vo
@dirrm lib/coq/contrib7/fourier
lib/coq/contrib7/omega/Omega.vo
lib/coq/contrib7/omega/OmegaLemmas.vo
@dirrm lib/coq/contrib7/omega
lib/coq/contrib7/ring/ArithRing.vo
lib/coq/contrib7/ring/NArithRing.vo
lib/coq/contrib7/ring/Quote.vo

lib/coq/contrib7/ring/Setoid_ring_normalize.vo
lib/coq/contrib7/ring/Setoid_ring_theory.vo
lib/coq/contrib7/ring/ZArithRing.vo
@dirrm lib/coq/contrib7/ring
lib/coq/contrib7/romega/ROmega.vo
lib/coq/contrib7/romega/ReflOmegaCore.vo
@dirrm lib/coq/contrib7/romega
@dirrm lib/coq/contrib7
lib/coq/ide/.coqide-gtk2rc
lib/coq/ide/FAQ
lib/coq/ide/coq.png
lib/coq/ide/utf8.v
lib/coq/ide/utf8.vo
@dirrm lib/coq/ide
lib/coq/states/initial.coq
@dirrm lib/coq/states
lib/coq/states7/barestate.coq
lib/coq/states7/initial.coq
@dirrm lib/coq/states7
lib/coq/theories/Arith/Arith.vo
lib/coq/theories/Arith/Between.vo
lib/coq/theories/Arith/Bool_nat.vo

lib/coq/theories/Arith/Peano_dec.vo
lib/coq/theories/Arith/Plus.vo
lib/coq/theories/Arith/Wf_nat.vo
@dirrm lib/coq/theories/Arith
lib/coq/theories/Bool/Bool.vo
lib/coq/theories/Bool/BoolEq.vo
lib/coq/theories/Bool/Bvector.vo

lib/coq/theories/Bool/IfProp.vo
lib/coq/theories/Bool/Sumbool.vo
lib/coq/theories/Bool/Zerob.vo
@dirrm lib/coq/theories/Bool
lib/coq/theories/Init/Datatypes.vo
lib/coq/theories/Init/Logic.vo
lib/coq/theories/Init/Logic_Type.vo

lib/coq/theories/Init/Prelude.vo
lib/coq/theories/Init/Specif.vo
lib/coq/theories/Init/Wf.vo
@dirrm lib/coq/theories/Init
lib/coq/theories/IntMap/Adalloc.vo
lib/coq/theories/IntMap/Addec.vo
lib/coq/theories/IntMap/Addr.vo

lib/coq/theories/IntMap/Mapiter.vo
lib/coq/theories/IntMap/Maplists.vo
lib/coq/theories/IntMap/Mapsubset.vo
@dirrm lib/coq/theories/IntMap
lib/coq/theories/Lists/List.vo
lib/coq/theories/Lists/ListSet.vo
lib/coq/theories/Lists/MonoList.vo
lib/coq/theories/Lists/Streams.vo
lib/coq/theories/Lists/TheoryList.vo
@dirrm lib/coq/theories/Lists
lib/coq/theories/Logic/Berardi.vo
lib/coq/theories/Logic/ChoiceFacts.vo
lib/coq/theories/Logic/Classical.vo

lib/coq/theories/Logic/JMeq.vo
lib/coq/theories/Logic/ProofIrrelevance.vo
lib/coq/theories/Logic/RelationalChoice.vo
@dirrm lib/coq/theories/Logic
lib/coq/theories/NArith/BinNat.vo
lib/coq/theories/NArith/BinPos.vo
lib/coq/theories/NArith/NArith.vo
lib/coq/theories/NArith/Pnat.vo
@dirrm lib/coq/theories/NArith
lib/coq/theories/Reals/Alembert.vo
lib/coq/theories/Reals/AltSeries.vo
lib/coq/theories/Reals/ArithProp.vo

lib/coq/theories/Reals/SplitAbsolu.vo
lib/coq/theories/Reals/SplitRmult.vo
lib/coq/theories/Reals/Sqrt_reg.vo
@dirrm lib/coq/theories/Reals
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
@dirrm lib/coq/theories/Relations
lib/coq/theories/Setoids/Setoid.vo
@dirrm lib/coq/theories/Setoids
lib/coq/theories/Sets/Classical_sets.vo
lib/coq/theories/Sets/Constructive_sets.vo
lib/coq/theories/Sets/Cpo.vo

lib/coq/theories/Sets/Relations_3.vo
lib/coq/theories/Sets/Relations_3_facts.vo
lib/coq/theories/Sets/Uniset.vo
@dirrm lib/coq/theories/Sets
lib/coq/theories/Sorting/Heap.vo
lib/coq/theories/Sorting/Permutation.vo
lib/coq/theories/Sorting/Sorting.vo
@dirrm lib/coq/theories/Sorting
lib/coq/theories/Wellfounded/Disjoint_Union.vo
lib/coq/theories/Wellfounded/Inclusion.vo
lib/coq/theories/Wellfounded/Inverse_Image.vo

lib/coq/theories/Wellfounded/Union.vo
lib/coq/theories/Wellfounded/Well_Ordering.vo
lib/coq/theories/Wellfounded/Wellfounded.vo
@dirrm lib/coq/theories/Wellfounded
lib/coq/theories/ZArith/BinInt.vo
lib/coq/theories/ZArith/Wf_Z.vo
lib/coq/theories/ZArith/ZArith.vo

lib/coq/theories/ZArith/Zsqrt.vo
lib/coq/theories/ZArith/Zwf.vo
lib/coq/theories/ZArith/auxiliary.vo
@dirrm lib/coq/theories/ZArith
@dirrm lib/coq/theories
lib/coq/theories7/Arith/Arith.vo
lib/coq/theories7/Arith/Between.vo
lib/coq/theories7/Arith/Bool_nat.vo

lib/coq/theories7/Arith/Peano_dec.vo
lib/coq/theories7/Arith/Plus.vo
lib/coq/theories7/Arith/Wf_nat.vo
@dirrm lib/coq/theories7/Arith
lib/coq/theories7/Bool/Bool.vo
lib/coq/theories7/Bool/BoolEq.vo
lib/coq/theories7/Bool/Bvector.vo

lib/coq/theories7/Bool/IfProp.vo
lib/coq/theories7/Bool/Sumbool.vo
lib/coq/theories7/Bool/Zerob.vo
@dirrm lib/coq/theories7/Bool
lib/coq/theories7/Init/Datatypes.vo
lib/coq/theories7/Init/Logic.vo
lib/coq/theories7/Init/Logic_Type.vo

lib/coq/theories7/Init/Prelude.vo
lib/coq/theories7/Init/Specif.vo
lib/coq/theories7/Init/Wf.vo
@dirrm lib/coq/theories7/Init
lib/coq/theories7/IntMap/Adalloc.vo
lib/coq/theories7/IntMap/Addec.vo
lib/coq/theories7/IntMap/Addr.vo

lib/coq/theories7/IntMap/Mapiter.vo
lib/coq/theories7/IntMap/Maplists.vo
lib/coq/theories7/IntMap/Mapsubset.vo
@dirrm lib/coq/theories7/IntMap
lib/coq/theories7/Lists/List.vo
lib/coq/theories7/Lists/ListSet.vo
lib/coq/theories7/Lists/MonoList.vo

lib/coq/theories7/Lists/PolyListSyntax.vo
lib/coq/theories7/Lists/Streams.vo
lib/coq/theories7/Lists/TheoryList.vo
@dirrm lib/coq/theories7/Lists
lib/coq/theories7/Logic/Berardi.vo
lib/coq/theories7/Logic/ChoiceFacts.vo
lib/coq/theories7/Logic/Classical.vo

lib/coq/theories7/Logic/JMeq.vo
lib/coq/theories7/Logic/ProofIrrelevance.vo
lib/coq/theories7/Logic/RelationalChoice.vo
@dirrm lib/coq/theories7/Logic
lib/coq/theories7/NArith/BinNat.vo
lib/coq/theories7/NArith/BinPos.vo
lib/coq/theories7/NArith/NArith.vo
lib/coq/theories7/NArith/Pnat.vo
@dirrm lib/coq/theories7/NArith
lib/coq/theories7/Reals/Alembert.vo
lib/coq/theories7/Reals/AltSeries.vo
lib/coq/theories7/Reals/ArithProp.vo

lib/coq/theories7/Reals/SplitAbsolu.vo
lib/coq/theories7/Reals/SplitRmult.vo
lib/coq/theories7/Reals/Sqrt_reg.vo
@dirrm lib/coq/theories7/Reals
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
@dirrm lib/coq/theories7/Relations
lib/coq/theories7/Setoids/Setoid.vo
@dirrm lib/coq/theories7/Setoids
lib/coq/theories7/Sets/Classical_sets.vo
lib/coq/theories7/Sets/Constructive_sets.vo
lib/coq/theories7/Sets/Cpo.vo

lib/coq/theories7/Sets/Relations_3.vo
lib/coq/theories7/Sets/Relations_3_facts.vo
lib/coq/theories7/Sets/Uniset.vo
@dirrm lib/coq/theories7/Sets
lib/coq/theories7/Sorting/Heap.vo
lib/coq/theories7/Sorting/Permutation.vo
lib/coq/theories7/Sorting/Sorting.vo
@dirrm lib/coq/theories7/Sorting
lib/coq/theories7/Wellfounded/Disjoint_Union.vo
lib/coq/theories7/Wellfounded/Inclusion.vo
lib/coq/theories7/Wellfounded/Inverse_Image.vo

lib/coq/theories7/Wellfounded/Union.vo
lib/coq/theories7/Wellfounded/Well_Ordering.vo
lib/coq/theories7/Wellfounded/Wellfounded.vo
@dirrm lib/coq/theories7/Wellfounded
lib/coq/theories7/ZArith/BinInt.vo
lib/coq/theories7/ZArith/Wf_Z.vo
lib/coq/theories7/ZArith/ZArith.vo

lib/coq/theories7/ZArith/auxiliary.vo
lib/coq/theories7/ZArith/fast_integer.vo
lib/coq/theories7/ZArith/zarith_aux.vo
@dirrm lib/coq/theories7/ZArith
@dirrm lib/coq/theories7
@dirrm lib/coq
share/emacs/site-lisp/coq-inferior.el
share/emacs/site-lisp/coq.el
share/texmf/tex/latex/misc/coqdoc.sty

%%PORTDOCS%%%%DOCSDIR%%/LICENSE
%%PORTDOCS%%%%DOCSDIR%%/README
%%PORTDOCS%%@dirrm %%DOCSDIR%%
@dirrm lib/coq/contrib/cc
@dirrm lib/coq/contrib/field
@dirrm lib/coq/contrib/fourier
@dirrm lib/coq/contrib/interface
@dirrm lib/coq/contrib/omega
@dirrm lib/coq/contrib/ring
@dirrm lib/coq/contrib/romega
@dirrm lib/coq/contrib
@dirrm lib/coq/contrib7/cc
@dirrm lib/coq/contrib7/field
@dirrm lib/coq/contrib7/fourier
@dirrm lib/coq/contrib7/omega
@dirrm lib/coq/contrib7/ring
@dirrm lib/coq/contrib7/romega
@dirrm lib/coq/contrib7
@dirrm lib/coq/ide
@dirrm lib/coq/states
@dirrm lib/coq/states7
@dirrm lib/coq/theories/Arith
@dirrm lib/coq/theories/Bool
@dirrm lib/coq/theories/Init
@dirrm lib/coq/theories/IntMap
@dirrm lib/coq/theories/Lists
@dirrm lib/coq/theories/Logic
@dirrm lib/coq/theories/NArith
@dirrm lib/coq/theories/Reals
@dirrm lib/coq/theories/Relations
@dirrm lib/coq/theories/Setoids
@dirrm lib/coq/theories/Sets
@dirrm lib/coq/theories/Sorting
@dirrm lib/coq/theories/Wellfounded
@dirrm lib/coq/theories/ZArith
@dirrm lib/coq/theories
@dirrm lib/coq/theories7/Arith
@dirrm lib/coq/theories7/Bool
@dirrm lib/coq/theories7/Init
@dirrm lib/coq/theories7/IntMap
@dirrm lib/coq/theories7/Lists
@dirrm lib/coq/theories7/Logic
@dirrm lib/coq/theories7/NArith
@dirrm lib/coq/theories7/Reals
@dirrm lib/coq/theories7/Relations
@dirrm lib/coq/theories7/Setoids
@dirrm lib/coq/theories7/Sets
@dirrm lib/coq/theories7/Sorting
@dirrm lib/coq/theories7/Wellfounded
@dirrm lib/coq/theories7/ZArith
@dirrm lib/coq/theories7
@dirrm lib/coq

Return to bug 73634

Lines 6-18 Link Here

(-)/usr/ports/math/coq/Makefile (-7 / +16 lines)
6	#	6	#
7		7
8	PORTNAME= coq	8	PORTNAME= coq
9	PORTVERSION= 8.0	9	PORTVERSION= 8.0p1
10	CATEGORIES= math	10	CATEGORIES= math
11	MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/	11	MASTER_SITES= ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/
12	DISTNAME= coq-8.0pl1	12	DISTNAME= coq-8.0pl1
13		13
14	PATCH_SITES= ${MASTER_SITES}	14	PATCH_SITES= ${MASTER_SITES}
15	#Ports has Ocaml 3.08.1 :	15	#only for Ocaml 3.08.1 :
16	PATCHFILES= patch-coq-8.0pl1-ocaml-3.08.1	16	PATCHFILES= patch-coq-8.0pl1-ocaml-3.08.1
17		17
18	MAINTAINER= r.c.ladan@student.tue.nl	18	MAINTAINER= r.c.ladan@student.tue.nl
Lines 29-39 Link Here
29	CONFIGURE_ARGS+= --opt	29	CONFIGURE_ARGS+= --opt
30		30
31	ALL_TARGET= world	31	ALL_TARGET= world
32	#no lablgl2 in ports yet
33		32
34	MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 \	33	.include <bsd.port.pre.mk>
35	coqdoc.1 coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 \	34
36	coqwc.1 parser.1 gallina.1	35	.if exists(${LOCALBASE}/bin/lablgtk2)
		36	BUILD_DEPENDS+= lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2
		37	RUN_DEPENDS+= ${BUILD_DEPENDS}
		38	PLIST_SUB+= IDE=""
		39	.else
		40	PLIST_SUB+= IDE="@comment "
		41	.endif
		42
		43	MAN1= coq-interface.1 coq-tex.1 coq_makefile.1 coqc.1 coqdep.1 coqdoc.1 \
		44	coqmktop.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqwc.1 gallina.1 \
		45	parser.1
37		46
38	post-install:	47	post-install:
39	.if !defined(NOPORTDOCS)	48	.if !defined(NOPORTDOCS)
Lines 43-46 Link Here
43	.endfor	52	.endfor
44	.endif	53	.endif
45		54
46	.include <bsd.port.mk>	55	.include <bsd.port.post.mk>

Lines 1-4 Link Here

(-)/usr/ports/math/coq/pkg-plist (-50 / +52 lines)
1	@comment $FreeBSD: ports/math/coq/pkg-plist,v 1.1 2004/10/16 00:55:32 pav Exp $
2	bin/coq-interface	1	bin/coq-interface
3	bin/coq-interface.opt	2	bin/coq-interface.opt
4	bin/coq-tex	3	bin/coq-tex
Lines 6-11 Link Here
6	bin/coqc	5	bin/coqc
7	bin/coqdep	6	bin/coqdep
8	bin/coqdoc	7	bin/coqdoc
		8	%%IDE%%bin/coqide
		9	%%IDE%%bin/coqide.byte
		10	%%IDE%%bin/coqide.opt
9	bin/coqmktop	11	bin/coqmktop
10	bin/coqtop	12	bin/coqtop
11	bin/coqtop.byte	13	bin/coqtop.byte
Lines 15-29 Link Here
15	bin/parser	17	bin/parser
16	bin/parser.opt	18	bin/parser.opt
17	lib/coq/contrib/cc/CCSolve.vo	19	lib/coq/contrib/cc/CCSolve.vo
		20	@dirrm lib/coq/contrib/cc
18	lib/coq/contrib/field/Field.vo	21	lib/coq/contrib/field/Field.vo
19	lib/coq/contrib/field/Field_Compl.vo	22	lib/coq/contrib/field/Field_Compl.vo
20	lib/coq/contrib/field/Field_Tactic.vo	23	lib/coq/contrib/field/Field_Tactic.vo
21	lib/coq/contrib/field/Field_Theory.vo	24	lib/coq/contrib/field/Field_Theory.vo
		25	@dirrm lib/coq/contrib/field
22	lib/coq/contrib/fourier/Fourier.vo	26	lib/coq/contrib/fourier/Fourier.vo
23	lib/coq/contrib/fourier/Fourier_util.vo	27	lib/coq/contrib/fourier/Fourier_util.vo
		28	@dirrm lib/coq/contrib/fourier
24	lib/coq/contrib/interface/vernacrc	29	lib/coq/contrib/interface/vernacrc
		30	@dirrm lib/coq/contrib/interface
25	lib/coq/contrib/omega/Omega.vo	31	lib/coq/contrib/omega/Omega.vo
26	lib/coq/contrib/omega/OmegaLemmas.vo	32	lib/coq/contrib/omega/OmegaLemmas.vo
		33	@dirrm lib/coq/contrib/omega
27	lib/coq/contrib/ring/ArithRing.vo	34	lib/coq/contrib/ring/ArithRing.vo
28	lib/coq/contrib/ring/NArithRing.vo	35	lib/coq/contrib/ring/NArithRing.vo
29	lib/coq/contrib/ring/Quote.vo	36	lib/coq/contrib/ring/Quote.vo
Lines 35-51 Link Here
35	lib/coq/contrib/ring/Setoid_ring_normalize.vo	42	lib/coq/contrib/ring/Setoid_ring_normalize.vo
36	lib/coq/contrib/ring/Setoid_ring_theory.vo	43	lib/coq/contrib/ring/Setoid_ring_theory.vo
37	lib/coq/contrib/ring/ZArithRing.vo	44	lib/coq/contrib/ring/ZArithRing.vo
		45	@dirrm lib/coq/contrib/ring
38	lib/coq/contrib/romega/ROmega.vo	46	lib/coq/contrib/romega/ROmega.vo
39	lib/coq/contrib/romega/ReflOmegaCore.vo	47	lib/coq/contrib/romega/ReflOmegaCore.vo
		48	@dirrm lib/coq/contrib/romega
		49	@dirrm lib/coq/contrib
40	lib/coq/contrib7/cc/CCSolve.vo	50	lib/coq/contrib7/cc/CCSolve.vo
		51	@dirrm lib/coq/contrib7/cc
41	lib/coq/contrib7/field/Field.vo	52	lib/coq/contrib7/field/Field.vo
42	lib/coq/contrib7/field/Field_Compl.vo	53	lib/coq/contrib7/field/Field_Compl.vo
43	lib/coq/contrib7/field/Field_Tactic.vo	54	lib/coq/contrib7/field/Field_Tactic.vo
44	lib/coq/contrib7/field/Field_Theory.vo	55	lib/coq/contrib7/field/Field_Theory.vo
		56	@dirrm lib/coq/contrib7/field
45	lib/coq/contrib7/fourier/Fourier.vo	57	lib/coq/contrib7/fourier/Fourier.vo
46	lib/coq/contrib7/fourier/Fourier_util.vo	58	lib/coq/contrib7/fourier/Fourier_util.vo
		59	@dirrm lib/coq/contrib7/fourier
47	lib/coq/contrib7/omega/Omega.vo	60	lib/coq/contrib7/omega/Omega.vo
48	lib/coq/contrib7/omega/OmegaLemmas.vo	61	lib/coq/contrib7/omega/OmegaLemmas.vo
		62	@dirrm lib/coq/contrib7/omega
49	lib/coq/contrib7/ring/ArithRing.vo	63	lib/coq/contrib7/ring/ArithRing.vo
50	lib/coq/contrib7/ring/NArithRing.vo	64	lib/coq/contrib7/ring/NArithRing.vo
51	lib/coq/contrib7/ring/Quote.vo	65	lib/coq/contrib7/ring/Quote.vo
Lines 57-72 Link Here
57	lib/coq/contrib7/ring/Setoid_ring_normalize.vo	71	lib/coq/contrib7/ring/Setoid_ring_normalize.vo
58	lib/coq/contrib7/ring/Setoid_ring_theory.vo	72	lib/coq/contrib7/ring/Setoid_ring_theory.vo
59	lib/coq/contrib7/ring/ZArithRing.vo	73	lib/coq/contrib7/ring/ZArithRing.vo
		74	@dirrm lib/coq/contrib7/ring
60	lib/coq/contrib7/romega/ROmega.vo	75	lib/coq/contrib7/romega/ROmega.vo
61	lib/coq/contrib7/romega/ReflOmegaCore.vo	76	lib/coq/contrib7/romega/ReflOmegaCore.vo
		77	@dirrm lib/coq/contrib7/romega
		78	@dirrm lib/coq/contrib7
62	lib/coq/ide/.coqide-gtk2rc	79	lib/coq/ide/.coqide-gtk2rc
63	lib/coq/ide/FAQ	80	lib/coq/ide/FAQ
64	lib/coq/ide/coq.png	81	lib/coq/ide/coq.png
65	lib/coq/ide/utf8.v	82	lib/coq/ide/utf8.v
66	lib/coq/ide/utf8.vo	83	lib/coq/ide/utf8.vo
		84	@dirrm lib/coq/ide
67	lib/coq/states/initial.coq	85	lib/coq/states/initial.coq
		86	@dirrm lib/coq/states
68	lib/coq/states7/barestate.coq	87	lib/coq/states7/barestate.coq
69	lib/coq/states7/initial.coq	88	lib/coq/states7/initial.coq
		89	@dirrm lib/coq/states7
70	lib/coq/theories/Arith/Arith.vo	90	lib/coq/theories/Arith/Arith.vo
71	lib/coq/theories/Arith/Between.vo	91	lib/coq/theories/Arith/Between.vo
72	lib/coq/theories/Arith/Bool_nat.vo	92	lib/coq/theories/Arith/Bool_nat.vo
Lines 87-92 Link Here
87	lib/coq/theories/Arith/Peano_dec.vo	107	lib/coq/theories/Arith/Peano_dec.vo
88	lib/coq/theories/Arith/Plus.vo	108	lib/coq/theories/Arith/Plus.vo
89	lib/coq/theories/Arith/Wf_nat.vo	109	lib/coq/theories/Arith/Wf_nat.vo
		110	@dirrm lib/coq/theories/Arith
90	lib/coq/theories/Bool/Bool.vo	111	lib/coq/theories/Bool/Bool.vo
91	lib/coq/theories/Bool/BoolEq.vo	112	lib/coq/theories/Bool/BoolEq.vo
92	lib/coq/theories/Bool/Bvector.vo	113	lib/coq/theories/Bool/Bvector.vo
Lines 94-99 Link Here
94	lib/coq/theories/Bool/IfProp.vo	115	lib/coq/theories/Bool/IfProp.vo
95	lib/coq/theories/Bool/Sumbool.vo	116	lib/coq/theories/Bool/Sumbool.vo
96	lib/coq/theories/Bool/Zerob.vo	117	lib/coq/theories/Bool/Zerob.vo
		118	@dirrm lib/coq/theories/Bool
97	lib/coq/theories/Init/Datatypes.vo	119	lib/coq/theories/Init/Datatypes.vo
98	lib/coq/theories/Init/Logic.vo	120	lib/coq/theories/Init/Logic.vo
99	lib/coq/theories/Init/Logic_Type.vo	121	lib/coq/theories/Init/Logic_Type.vo
Lines 102-107 Link Here
102	lib/coq/theories/Init/Prelude.vo	124	lib/coq/theories/Init/Prelude.vo
103	lib/coq/theories/Init/Specif.vo	125	lib/coq/theories/Init/Specif.vo
104	lib/coq/theories/Init/Wf.vo	126	lib/coq/theories/Init/Wf.vo
		127	@dirrm lib/coq/theories/Init
105	lib/coq/theories/IntMap/Adalloc.vo	128	lib/coq/theories/IntMap/Adalloc.vo
106	lib/coq/theories/IntMap/Addec.vo	129	lib/coq/theories/IntMap/Addec.vo
107	lib/coq/theories/IntMap/Addr.vo	130	lib/coq/theories/IntMap/Addr.vo
Lines 118-128 Link Here
118	lib/coq/theories/IntMap/Mapiter.vo	141	lib/coq/theories/IntMap/Mapiter.vo
119	lib/coq/theories/IntMap/Maplists.vo	142	lib/coq/theories/IntMap/Maplists.vo
120	lib/coq/theories/IntMap/Mapsubset.vo	143	lib/coq/theories/IntMap/Mapsubset.vo
		144	@dirrm lib/coq/theories/IntMap
121	lib/coq/theories/Lists/List.vo	145	lib/coq/theories/Lists/List.vo
122	lib/coq/theories/Lists/ListSet.vo	146	lib/coq/theories/Lists/ListSet.vo
123	lib/coq/theories/Lists/MonoList.vo	147	lib/coq/theories/Lists/MonoList.vo
124	lib/coq/theories/Lists/Streams.vo	148	lib/coq/theories/Lists/Streams.vo
125	lib/coq/theories/Lists/TheoryList.vo	149	lib/coq/theories/Lists/TheoryList.vo
		150	@dirrm lib/coq/theories/Lists
126	lib/coq/theories/Logic/Berardi.vo	151	lib/coq/theories/Logic/Berardi.vo
127	lib/coq/theories/Logic/ChoiceFacts.vo	152	lib/coq/theories/Logic/ChoiceFacts.vo
128	lib/coq/theories/Logic/Classical.vo	153	lib/coq/theories/Logic/Classical.vo
Lines 141-150 Link Here
141	lib/coq/theories/Logic/JMeq.vo	166	lib/coq/theories/Logic/JMeq.vo
142	lib/coq/theories/Logic/ProofIrrelevance.vo	167	lib/coq/theories/Logic/ProofIrrelevance.vo
143	lib/coq/theories/Logic/RelationalChoice.vo	168	lib/coq/theories/Logic/RelationalChoice.vo
		169	@dirrm lib/coq/theories/Logic
144	lib/coq/theories/NArith/BinNat.vo	170	lib/coq/theories/NArith/BinNat.vo
145	lib/coq/theories/NArith/BinPos.vo	171	lib/coq/theories/NArith/BinPos.vo
146	lib/coq/theories/NArith/NArith.vo	172	lib/coq/theories/NArith/NArith.vo
147	lib/coq/theories/NArith/Pnat.vo	173	lib/coq/theories/NArith/Pnat.vo
		174	@dirrm lib/coq/theories/NArith
148	lib/coq/theories/Reals/Alembert.vo	175	lib/coq/theories/Reals/Alembert.vo
149	lib/coq/theories/Reals/AltSeries.vo	176	lib/coq/theories/Reals/AltSeries.vo
150	lib/coq/theories/Reals/ArithProp.vo	177	lib/coq/theories/Reals/ArithProp.vo
Lines 198-210 Link Here
198	lib/coq/theories/Reals/SplitAbsolu.vo	225	lib/coq/theories/Reals/SplitAbsolu.vo
199	lib/coq/theories/Reals/SplitRmult.vo	226	lib/coq/theories/Reals/SplitRmult.vo
200	lib/coq/theories/Reals/Sqrt_reg.vo	227	lib/coq/theories/Reals/Sqrt_reg.vo
		228	@dirrm lib/coq/theories/Reals
201	lib/coq/theories/Relations/Newman.vo	229	lib/coq/theories/Relations/Newman.vo
202	lib/coq/theories/Relations/Operators_Properties.vo	230	lib/coq/theories/Relations/Operators_Properties.vo
203	lib/coq/theories/Relations/Relation_Definitions.vo	231	lib/coq/theories/Relations/Relation_Definitions.vo
204	lib/coq/theories/Relations/Relation_Operators.vo	232	lib/coq/theories/Relations/Relation_Operators.vo
205	lib/coq/theories/Relations/Relations.vo	233	lib/coq/theories/Relations/Relations.vo
206	lib/coq/theories/Relations/Rstar.vo	234	lib/coq/theories/Relations/Rstar.vo
		235	@dirrm lib/coq/theories/Relations
207	lib/coq/theories/Setoids/Setoid.vo	236	lib/coq/theories/Setoids/Setoid.vo
		237	@dirrm lib/coq/theories/Setoids
208	lib/coq/theories/Sets/Classical_sets.vo	238	lib/coq/theories/Sets/Classical_sets.vo
209	lib/coq/theories/Sets/Constructive_sets.vo	239	lib/coq/theories/Sets/Constructive_sets.vo
210	lib/coq/theories/Sets/Cpo.vo	240	lib/coq/theories/Sets/Cpo.vo
Lines 227-235 Link Here
227	lib/coq/theories/Sets/Relations_3.vo	257	lib/coq/theories/Sets/Relations_3.vo
228	lib/coq/theories/Sets/Relations_3_facts.vo	258	lib/coq/theories/Sets/Relations_3_facts.vo
229	lib/coq/theories/Sets/Uniset.vo	259	lib/coq/theories/Sets/Uniset.vo
		260	@dirrm lib/coq/theories/Sets
230	lib/coq/theories/Sorting/Heap.vo	261	lib/coq/theories/Sorting/Heap.vo
231	lib/coq/theories/Sorting/Permutation.vo	262	lib/coq/theories/Sorting/Permutation.vo
232	lib/coq/theories/Sorting/Sorting.vo	263	lib/coq/theories/Sorting/Sorting.vo
		264	@dirrm lib/coq/theories/Sorting
233	lib/coq/theories/Wellfounded/Disjoint_Union.vo	265	lib/coq/theories/Wellfounded/Disjoint_Union.vo
234	lib/coq/theories/Wellfounded/Inclusion.vo	266	lib/coq/theories/Wellfounded/Inclusion.vo
235	lib/coq/theories/Wellfounded/Inverse_Image.vo	267	lib/coq/theories/Wellfounded/Inverse_Image.vo
Lines 239-244 Link Here
239	lib/coq/theories/Wellfounded/Union.vo	271	lib/coq/theories/Wellfounded/Union.vo
240	lib/coq/theories/Wellfounded/Well_Ordering.vo	272	lib/coq/theories/Wellfounded/Well_Ordering.vo
241	lib/coq/theories/Wellfounded/Wellfounded.vo	273	lib/coq/theories/Wellfounded/Wellfounded.vo
		274	@dirrm lib/coq/theories/Wellfounded
242	lib/coq/theories/ZArith/BinInt.vo	275	lib/coq/theories/ZArith/BinInt.vo
243	lib/coq/theories/ZArith/Wf_Z.vo	276	lib/coq/theories/ZArith/Wf_Z.vo
244	lib/coq/theories/ZArith/ZArith.vo	277	lib/coq/theories/ZArith/ZArith.vo
Lines 262-267 Link Here
262	lib/coq/theories/ZArith/Zsqrt.vo	295	lib/coq/theories/ZArith/Zsqrt.vo
263	lib/coq/theories/ZArith/Zwf.vo	296	lib/coq/theories/ZArith/Zwf.vo
264	lib/coq/theories/ZArith/auxiliary.vo	297	lib/coq/theories/ZArith/auxiliary.vo
		298	@dirrm lib/coq/theories/ZArith
		299	@dirrm lib/coq/theories
265	lib/coq/theories7/Arith/Arith.vo	300	lib/coq/theories7/Arith/Arith.vo
266	lib/coq/theories7/Arith/Between.vo	301	lib/coq/theories7/Arith/Between.vo
267	lib/coq/theories7/Arith/Bool_nat.vo	302	lib/coq/theories7/Arith/Bool_nat.vo
Lines 282-287 Link Here
282	lib/coq/theories7/Arith/Peano_dec.vo	317	lib/coq/theories7/Arith/Peano_dec.vo
283	lib/coq/theories7/Arith/Plus.vo	318	lib/coq/theories7/Arith/Plus.vo
284	lib/coq/theories7/Arith/Wf_nat.vo	319	lib/coq/theories7/Arith/Wf_nat.vo
		320	@dirrm lib/coq/theories7/Arith
285	lib/coq/theories7/Bool/Bool.vo	321	lib/coq/theories7/Bool/Bool.vo
286	lib/coq/theories7/Bool/BoolEq.vo	322	lib/coq/theories7/Bool/BoolEq.vo
287	lib/coq/theories7/Bool/Bvector.vo	323	lib/coq/theories7/Bool/Bvector.vo
Lines 289-294 Link Here
289	lib/coq/theories7/Bool/IfProp.vo	325	lib/coq/theories7/Bool/IfProp.vo
290	lib/coq/theories7/Bool/Sumbool.vo	326	lib/coq/theories7/Bool/Sumbool.vo
291	lib/coq/theories7/Bool/Zerob.vo	327	lib/coq/theories7/Bool/Zerob.vo
		328	@dirrm lib/coq/theories7/Bool
292	lib/coq/theories7/Init/Datatypes.vo	329	lib/coq/theories7/Init/Datatypes.vo
293	lib/coq/theories7/Init/Logic.vo	330	lib/coq/theories7/Init/Logic.vo
294	lib/coq/theories7/Init/Logic_Type.vo	331	lib/coq/theories7/Init/Logic_Type.vo
Lines 297-302 Link Here
297	lib/coq/theories7/Init/Prelude.vo	334	lib/coq/theories7/Init/Prelude.vo
298	lib/coq/theories7/Init/Specif.vo	335	lib/coq/theories7/Init/Specif.vo
299	lib/coq/theories7/Init/Wf.vo	336	lib/coq/theories7/Init/Wf.vo
		337	@dirrm lib/coq/theories7/Init
300	lib/coq/theories7/IntMap/Adalloc.vo	338	lib/coq/theories7/IntMap/Adalloc.vo
301	lib/coq/theories7/IntMap/Addec.vo	339	lib/coq/theories7/IntMap/Addec.vo
302	lib/coq/theories7/IntMap/Addr.vo	340	lib/coq/theories7/IntMap/Addr.vo
Lines 313-318 Link Here
313	lib/coq/theories7/IntMap/Mapiter.vo	351	lib/coq/theories7/IntMap/Mapiter.vo
314	lib/coq/theories7/IntMap/Maplists.vo	352	lib/coq/theories7/IntMap/Maplists.vo
315	lib/coq/theories7/IntMap/Mapsubset.vo	353	lib/coq/theories7/IntMap/Mapsubset.vo
		354	@dirrm lib/coq/theories7/IntMap
316	lib/coq/theories7/Lists/List.vo	355	lib/coq/theories7/Lists/List.vo
317	lib/coq/theories7/Lists/ListSet.vo	356	lib/coq/theories7/Lists/ListSet.vo
318	lib/coq/theories7/Lists/MonoList.vo	357	lib/coq/theories7/Lists/MonoList.vo
Lines 320-325 Link Here
320	lib/coq/theories7/Lists/PolyListSyntax.vo	359	lib/coq/theories7/Lists/PolyListSyntax.vo
321	lib/coq/theories7/Lists/Streams.vo	360	lib/coq/theories7/Lists/Streams.vo
322	lib/coq/theories7/Lists/TheoryList.vo	361	lib/coq/theories7/Lists/TheoryList.vo
		362	@dirrm lib/coq/theories7/Lists
323	lib/coq/theories7/Logic/Berardi.vo	363	lib/coq/theories7/Logic/Berardi.vo
324	lib/coq/theories7/Logic/ChoiceFacts.vo	364	lib/coq/theories7/Logic/ChoiceFacts.vo
325	lib/coq/theories7/Logic/Classical.vo	365	lib/coq/theories7/Logic/Classical.vo
Lines 338-347 Link Here
338	lib/coq/theories7/Logic/JMeq.vo	378	lib/coq/theories7/Logic/JMeq.vo
339	lib/coq/theories7/Logic/ProofIrrelevance.vo	379	lib/coq/theories7/Logic/ProofIrrelevance.vo
340	lib/coq/theories7/Logic/RelationalChoice.vo	380	lib/coq/theories7/Logic/RelationalChoice.vo
		381	@dirrm lib/coq/theories7/Logic
341	lib/coq/theories7/NArith/BinNat.vo	382	lib/coq/theories7/NArith/BinNat.vo
342	lib/coq/theories7/NArith/BinPos.vo	383	lib/coq/theories7/NArith/BinPos.vo
343	lib/coq/theories7/NArith/NArith.vo	384	lib/coq/theories7/NArith/NArith.vo
344	lib/coq/theories7/NArith/Pnat.vo	385	lib/coq/theories7/NArith/Pnat.vo
		386	@dirrm lib/coq/theories7/NArith
345	lib/coq/theories7/Reals/Alembert.vo	387	lib/coq/theories7/Reals/Alembert.vo
346	lib/coq/theories7/Reals/AltSeries.vo	388	lib/coq/theories7/Reals/AltSeries.vo
347	lib/coq/theories7/Reals/ArithProp.vo	389	lib/coq/theories7/Reals/ArithProp.vo
Lines 396-408 Link Here
396	lib/coq/theories7/Reals/SplitAbsolu.vo	438	lib/coq/theories7/Reals/SplitAbsolu.vo
397	lib/coq/theories7/Reals/SplitRmult.vo	439	lib/coq/theories7/Reals/SplitRmult.vo
398	lib/coq/theories7/Reals/Sqrt_reg.vo	440	lib/coq/theories7/Reals/Sqrt_reg.vo
		441	@dirrm lib/coq/theories7/Reals
399	lib/coq/theories7/Relations/Newman.vo	442	lib/coq/theories7/Relations/Newman.vo
400	lib/coq/theories7/Relations/Operators_Properties.vo	443	lib/coq/theories7/Relations/Operators_Properties.vo
401	lib/coq/theories7/Relations/Relation_Definitions.vo	444	lib/coq/theories7/Relations/Relation_Definitions.vo
402	lib/coq/theories7/Relations/Relation_Operators.vo	445	lib/coq/theories7/Relations/Relation_Operators.vo
403	lib/coq/theories7/Relations/Relations.vo	446	lib/coq/theories7/Relations/Relations.vo
404	lib/coq/theories7/Relations/Rstar.vo	447	lib/coq/theories7/Relations/Rstar.vo
		448	@dirrm lib/coq/theories7/Relations
405	lib/coq/theories7/Setoids/Setoid.vo	449	lib/coq/theories7/Setoids/Setoid.vo
		450	@dirrm lib/coq/theories7/Setoids
406	lib/coq/theories7/Sets/Classical_sets.vo	451	lib/coq/theories7/Sets/Classical_sets.vo
407	lib/coq/theories7/Sets/Constructive_sets.vo	452	lib/coq/theories7/Sets/Constructive_sets.vo
408	lib/coq/theories7/Sets/Cpo.vo	453	lib/coq/theories7/Sets/Cpo.vo
Lines 425-433 Link Here
425	lib/coq/theories7/Sets/Relations_3.vo	470	lib/coq/theories7/Sets/Relations_3.vo
426	lib/coq/theories7/Sets/Relations_3_facts.vo	471	lib/coq/theories7/Sets/Relations_3_facts.vo
427	lib/coq/theories7/Sets/Uniset.vo	472	lib/coq/theories7/Sets/Uniset.vo
		473	@dirrm lib/coq/theories7/Sets
428	lib/coq/theories7/Sorting/Heap.vo	474	lib/coq/theories7/Sorting/Heap.vo
429	lib/coq/theories7/Sorting/Permutation.vo	475	lib/coq/theories7/Sorting/Permutation.vo
430	lib/coq/theories7/Sorting/Sorting.vo	476	lib/coq/theories7/Sorting/Sorting.vo
		477	@dirrm lib/coq/theories7/Sorting
431	lib/coq/theories7/Wellfounded/Disjoint_Union.vo	478	lib/coq/theories7/Wellfounded/Disjoint_Union.vo
432	lib/coq/theories7/Wellfounded/Inclusion.vo	479	lib/coq/theories7/Wellfounded/Inclusion.vo
433	lib/coq/theories7/Wellfounded/Inverse_Image.vo	480	lib/coq/theories7/Wellfounded/Inverse_Image.vo
Lines 437-442 Link Here
437	lib/coq/theories7/Wellfounded/Union.vo	484	lib/coq/theories7/Wellfounded/Union.vo
438	lib/coq/theories7/Wellfounded/Well_Ordering.vo	485	lib/coq/theories7/Wellfounded/Well_Ordering.vo
439	lib/coq/theories7/Wellfounded/Wellfounded.vo	486	lib/coq/theories7/Wellfounded/Wellfounded.vo
		487	@dirrm lib/coq/theories7/Wellfounded
440	lib/coq/theories7/ZArith/BinInt.vo	488	lib/coq/theories7/ZArith/BinInt.vo
441	lib/coq/theories7/ZArith/Wf_Z.vo	489	lib/coq/theories7/ZArith/Wf_Z.vo
442	lib/coq/theories7/ZArith/ZArith.vo	490	lib/coq/theories7/ZArith/ZArith.vo
Lines 463-468 Link Here
463	lib/coq/theories7/ZArith/auxiliary.vo	511	lib/coq/theories7/ZArith/auxiliary.vo
464	lib/coq/theories7/ZArith/fast_integer.vo	512	lib/coq/theories7/ZArith/fast_integer.vo
465	lib/coq/theories7/ZArith/zarith_aux.vo	513	lib/coq/theories7/ZArith/zarith_aux.vo
		514	@dirrm lib/coq/theories7/ZArith
		515	@dirrm lib/coq/theories7
		516	@dirrm lib/coq
466	share/emacs/site-lisp/coq-inferior.el	517	share/emacs/site-lisp/coq-inferior.el
467	share/emacs/site-lisp/coq.el	518	share/emacs/site-lisp/coq.el
468	share/texmf/tex/latex/misc/coqdoc.sty	519	share/texmf/tex/latex/misc/coqdoc.sty
Lines 473-524 Link Here
473	%%PORTDOCS%%%%DOCSDIR%%/LICENSE	524	%%PORTDOCS%%%%DOCSDIR%%/LICENSE
474	%%PORTDOCS%%%%DOCSDIR%%/README	525	%%PORTDOCS%%%%DOCSDIR%%/README
475	%%PORTDOCS%%@dirrm %%DOCSDIR%%	526	%%PORTDOCS%%@dirrm %%DOCSDIR%%
476	@dirrm lib/coq/contrib/cc
477	@dirrm lib/coq/contrib/field
478	@dirrm lib/coq/contrib/fourier
479	@dirrm lib/coq/contrib/interface
480	@dirrm lib/coq/contrib/omega
481	@dirrm lib/coq/contrib/ring
482	@dirrm lib/coq/contrib/romega
483	@dirrm lib/coq/contrib
484	@dirrm lib/coq/contrib7/cc
485	@dirrm lib/coq/contrib7/field
486	@dirrm lib/coq/contrib7/fourier
487	@dirrm lib/coq/contrib7/omega
488	@dirrm lib/coq/contrib7/ring
489	@dirrm lib/coq/contrib7/romega
490	@dirrm lib/coq/contrib7
491	@dirrm lib/coq/ide
492	@dirrm lib/coq/states
493	@dirrm lib/coq/states7
494	@dirrm lib/coq/theories/Arith
495	@dirrm lib/coq/theories/Bool
496	@dirrm lib/coq/theories/Init
497	@dirrm lib/coq/theories/IntMap
498	@dirrm lib/coq/theories/Lists
499	@dirrm lib/coq/theories/Logic
500	@dirrm lib/coq/theories/NArith
501	@dirrm lib/coq/theories/Reals
502	@dirrm lib/coq/theories/Relations
503	@dirrm lib/coq/theories/Setoids
504	@dirrm lib/coq/theories/Sets
505	@dirrm lib/coq/theories/Sorting
506	@dirrm lib/coq/theories/Wellfounded
507	@dirrm lib/coq/theories/ZArith
508	@dirrm lib/coq/theories
509	@dirrm lib/coq/theories7/Arith
510	@dirrm lib/coq/theories7/Bool
511	@dirrm lib/coq/theories7/Init
512	@dirrm lib/coq/theories7/IntMap
513	@dirrm lib/coq/theories7/Lists
514	@dirrm lib/coq/theories7/Logic
515	@dirrm lib/coq/theories7/NArith
516	@dirrm lib/coq/theories7/Reals
517	@dirrm lib/coq/theories7/Relations
518	@dirrm lib/coq/theories7/Setoids
519	@dirrm lib/coq/theories7/Sets
520	@dirrm lib/coq/theories7/Sorting
521	@dirrm lib/coq/theories7/Wellfounded
522	@dirrm lib/coq/theories7/ZArith
523	@dirrm lib/coq/theories7
524	@dirrm lib/coq