3367255cb4
Submitted by Yozo Toda <yozo@imit.chiba-u.ac.jp>. The Coq Proof Assistant is designed to write formal specifications, programs and to verify that programs are correct with respect to their specification.
377 lines
12 KiB
Plaintext
377 lines
12 KiB
Plaintext
@comment $OpenBSD: PLIST,v 1.1.1.1 2001/09/22 14:24:31 naddy Exp $
|
|
bin/coq-interface
|
|
bin/coq-tex
|
|
bin/coq_makefile
|
|
bin/coqc
|
|
bin/coqdep
|
|
bin/coqmktop
|
|
bin/coqtop
|
|
bin/coqtop.byte
|
|
bin/coqtop.opt
|
|
bin/gallina
|
|
bin/parser
|
|
lib/coq/contrib/correctness/ArrayPermut.vo
|
|
lib/coq/contrib/correctness/Arrays.vo
|
|
lib/coq/contrib/correctness/Correctness.vo
|
|
lib/coq/contrib/correctness/Exchange.vo
|
|
lib/coq/contrib/correctness/ProgBool.vo
|
|
lib/coq/contrib/correctness/ProgInt.vo
|
|
lib/coq/contrib/correctness/ProgWf.vo
|
|
lib/coq/contrib/correctness/Sorted.vo
|
|
lib/coq/contrib/correctness/Tuples.vo
|
|
lib/coq/contrib/extraction/Extraction.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/fourier/Fourier.vo
|
|
lib/coq/contrib/fourier/Fourier_util.vo
|
|
lib/coq/contrib/interface/Centaur.vo
|
|
lib/coq/contrib/interface/vernacrc
|
|
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/ZArithRing.vo
|
|
lib/coq/contrib/xml/Xml.vo
|
|
lib/coq/states/barestate.coq
|
|
lib/coq/states/initial.coq
|
|
lib/coq/tactics/AutoRewrite.vo
|
|
lib/coq/tactics/EAuto.vo
|
|
lib/coq/tactics/EqDecide.vo
|
|
lib/coq/tactics/Equality.vo
|
|
lib/coq/tactics/Inv.vo
|
|
lib/coq/tactics/Refine.vo
|
|
lib/coq/tactics/Tauto.vo
|
|
lib/coq/theories/Arith/Arith.vo
|
|
lib/coq/theories/Arith/Between.vo
|
|
lib/coq/theories/Arith/Compare.vo
|
|
lib/coq/theories/Arith/Compare_dec.vo
|
|
lib/coq/theories/Arith/Div2.vo
|
|
lib/coq/theories/Arith/EqNat.vo
|
|
lib/coq/theories/Arith/Euclid.vo
|
|
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/Min.vo
|
|
lib/coq/theories/Arith/Minus.vo
|
|
lib/coq/theories/Arith/Mult.vo
|
|
lib/coq/theories/Arith/Peano_dec.vo
|
|
lib/coq/theories/Arith/Plus.vo
|
|
lib/coq/theories/Arith/Wf_nat.vo
|
|
lib/coq/theories/Bool/Bool.vo
|
|
lib/coq/theories/Bool/BoolEq.vo
|
|
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/Init/Datatypes.vo
|
|
lib/coq/theories/Init/DatatypesSyntax.vo
|
|
lib/coq/theories/Init/Logic.vo
|
|
lib/coq/theories/Init/LogicSyntax.vo
|
|
lib/coq/theories/Init/Logic_Type.vo
|
|
lib/coq/theories/Init/Logic_TypeSyntax.vo
|
|
lib/coq/theories/Init/Peano.vo
|
|
lib/coq/theories/Init/Prelude.vo
|
|
lib/coq/theories/Init/Specif.vo
|
|
lib/coq/theories/Init/SpecifSyntax.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
|
|
lib/coq/theories/IntMap/Map.vo
|
|
lib/coq/theories/IntMap/Mapaxioms.vo
|
|
lib/coq/theories/IntMap/Mapc.vo
|
|
lib/coq/theories/IntMap/Mapcanon.vo
|
|
lib/coq/theories/IntMap/Mapcard.vo
|
|
lib/coq/theories/IntMap/Mapfold.vo
|
|
lib/coq/theories/IntMap/Mapiter.vo
|
|
lib/coq/theories/IntMap/Maplists.vo
|
|
lib/coq/theories/IntMap/Mapsubset.vo
|
|
lib/coq/theories/Lists/List.vo
|
|
lib/coq/theories/Lists/ListSet.vo
|
|
lib/coq/theories/Lists/PolyList.vo
|
|
lib/coq/theories/Lists/PolyListSyntax.vo
|
|
lib/coq/theories/Lists/Streams.vo
|
|
lib/coq/theories/Lists/TheoryList.vo
|
|
lib/coq/theories/Logic/Classical.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/Decidable.vo
|
|
lib/coq/theories/Logic/Eqdep.vo
|
|
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/Raxioms.vo
|
|
lib/coq/theories/Reals/Rbase.vo
|
|
lib/coq/theories/Reals/Rbasic_fun.vo
|
|
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/Rlimit.vo
|
|
lib/coq/theories/Reals/Rseries.vo
|
|
lib/coq/theories/Reals/Rsyntax.vo
|
|
lib/coq/theories/Reals/Rtrigo_fun.vo
|
|
lib/coq/theories/Reals/SplitAbsolu.vo
|
|
lib/coq/theories/Reals/SplitRmult.vo
|
|
lib/coq/theories/Reals/TypeSyntax.vo
|
|
lib/coq/theories/Relations/Newman.vo
|
|
lib/coq/theories/Relations/Operators_Properties.vo
|
|
lib/coq/theories/Relations/Relation_Definitions.vo
|
|
lib/coq/theories/Relations/Relation_Operators.vo
|
|
lib/coq/theories/Relations/Relations.vo
|
|
lib/coq/theories/Relations/Rstar.vo
|
|
lib/coq/theories/Sets/Classical_sets.vo
|
|
lib/coq/theories/Sets/Constructive_sets.vo
|
|
lib/coq/theories/Sets/Cpo.vo
|
|
lib/coq/theories/Sets/Ensembles.vo
|
|
lib/coq/theories/Sets/Finite_sets.vo
|
|
lib/coq/theories/Sets/Finite_sets_facts.vo
|
|
lib/coq/theories/Sets/Image.vo
|
|
lib/coq/theories/Sets/Infinite_sets.vo
|
|
lib/coq/theories/Sets/Integers.vo
|
|
lib/coq/theories/Sets/Multiset.vo
|
|
lib/coq/theories/Sets/Partial_Order.vo
|
|
lib/coq/theories/Sets/Permut.vo
|
|
lib/coq/theories/Sets/Powerset.vo
|
|
lib/coq/theories/Sets/Powerset_Classical_facts.vo
|
|
lib/coq/theories/Sets/Powerset_facts.vo
|
|
lib/coq/theories/Sets/Relations_1.vo
|
|
lib/coq/theories/Sets/Relations_1_facts.vo
|
|
lib/coq/theories/Sets/Relations_2.vo
|
|
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/Wellfounded/Disjoint_Union.vo
|
|
lib/coq/theories/Wellfounded/Inclusion.vo
|
|
lib/coq/theories/Wellfounded/Inverse_Image.vo
|
|
lib/coq/theories/Wellfounded/Lexicographic_Exponentiation.vo
|
|
lib/coq/theories/Wellfounded/Lexicographic_Product.vo
|
|
lib/coq/theories/Wellfounded/Transitive_Closure.vo
|
|
lib/coq/theories/Wellfounded/Union.vo
|
|
lib/coq/theories/Wellfounded/Well_Ordering.vo
|
|
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/Zmisc.vo
|
|
lib/coq/theories/ZArith/Zsyntax.vo
|
|
lib/coq/theories/ZArith/auxiliary.vo
|
|
lib/coq/theories/ZArith/fast_integer.vo
|
|
lib/coq/theories/ZArith/zarith_aux.vo
|
|
man/man1/coq-interface.1
|
|
man/man1/coq-tex.1
|
|
man/man1/coq_makefile.1
|
|
man/man1/coqc.1
|
|
man/man1/coqdep.1
|
|
man/man1/coqmktop.1
|
|
man/man1/coqtop.1
|
|
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/cover.html
|
|
share/doc/coq/html/main-0.html
|
|
share/doc/coq/html/main.html
|
|
share/doc/coq/html/next.gif
|
|
share/doc/coq/html/node.0.0.0.html
|
|
share/doc/coq/html/node.0.0.1.html
|
|
share/doc/coq/html/node.0.0.2.html
|
|
share/doc/coq/html/node.0.0.html
|
|
share/doc/coq/html/node.0.1.0.html
|
|
share/doc/coq/html/node.0.1.1.html
|
|
share/doc/coq/html/node.0.1.2.html
|
|
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.html
|
|
share/doc/coq/html/node.0.2.0.html
|
|
share/doc/coq/html/node.0.2.1.html
|
|
share/doc/coq/html/node.0.2.2.html
|
|
share/doc/coq/html/node.0.2.html
|
|
share/doc/coq/html/node.0.3.0.html
|
|
share/doc/coq/html/node.0.3.1.html
|
|
share/doc/coq/html/node.0.3.2.html
|
|
share/doc/coq/html/node.0.3.3.html
|
|
share/doc/coq/html/node.0.3.4.html
|
|
share/doc/coq/html/node.0.3.5.html
|
|
share/doc/coq/html/node.0.3.html
|
|
share/doc/coq/html/node.0.html
|
|
share/doc/coq/html/node.1.0.0.html
|
|
share/doc/coq/html/node.1.0.1.html
|
|
share/doc/coq/html/node.1.0.2.html
|
|
share/doc/coq/html/node.1.0.3.html
|
|
share/doc/coq/html/node.1.0.4.html
|
|
share/doc/coq/html/node.1.0.5.html
|
|
share/doc/coq/html/node.1.0.6.html
|
|
share/doc/coq/html/node.1.0.7.html
|
|
share/doc/coq/html/node.1.0.html
|
|
share/doc/coq/html/node.1.1.0.html
|
|
share/doc/coq/html/node.1.1.1.html
|
|
share/doc/coq/html/node.1.1.2.html
|
|
share/doc/coq/html/node.1.1.html
|
|
share/doc/coq/html/node.1.2.0.html
|
|
share/doc/coq/html/node.1.2.1.html
|
|
share/doc/coq/html/node.1.2.10.html
|
|
share/doc/coq/html/node.1.2.11.html
|
|
share/doc/coq/html/node.1.2.12.html
|
|
share/doc/coq/html/node.1.2.13.html
|
|
share/doc/coq/html/node.1.2.14.html
|
|
share/doc/coq/html/node.1.2.2.html
|
|
share/doc/coq/html/node.1.2.3.html
|
|
share/doc/coq/html/node.1.2.4.html
|
|
share/doc/coq/html/node.1.2.5.html
|
|
share/doc/coq/html/node.1.2.6.html
|
|
share/doc/coq/html/node.1.2.7.html
|
|
share/doc/coq/html/node.1.2.8.html
|
|
share/doc/coq/html/node.1.2.9.html
|
|
share/doc/coq/html/node.1.2.html
|
|
share/doc/coq/html/node.1.3.0.html
|
|
share/doc/coq/html/node.1.3.1.html
|
|
share/doc/coq/html/node.1.3.2.html
|
|
share/doc/coq/html/node.1.3.3.html
|
|
share/doc/coq/html/node.1.3.4.html
|
|
share/doc/coq/html/node.1.3.5.html
|
|
share/doc/coq/html/node.1.3.html
|
|
share/doc/coq/html/node.1.html
|
|
share/doc/coq/html/node.2.0.0.html
|
|
share/doc/coq/html/node.2.0.1.html
|
|
share/doc/coq/html/node.2.0.2.html
|
|
share/doc/coq/html/node.2.0.html
|
|
share/doc/coq/html/node.2.1.0.html
|
|
share/doc/coq/html/node.2.1.1.html
|
|
share/doc/coq/html/node.2.1.2.html
|
|
share/doc/coq/html/node.2.1.html
|
|
share/doc/coq/html/node.2.html
|
|
share/doc/coq/html/node.3.0.0.html
|
|
share/doc/coq/html/node.3.0.1.html
|
|
share/doc/coq/html/node.3.0.2.html
|
|
share/doc/coq/html/node.3.0.3.html
|
|
share/doc/coq/html/node.3.0.4.html
|
|
share/doc/coq/html/node.3.0.html
|
|
share/doc/coq/html/node.3.1.0.html
|
|
share/doc/coq/html/node.3.1.1.html
|
|
share/doc/coq/html/node.3.1.2.html
|
|
share/doc/coq/html/node.3.1.3.html
|
|
share/doc/coq/html/node.3.1.4.html
|
|
share/doc/coq/html/node.3.1.5.html
|
|
share/doc/coq/html/node.3.1.6.html
|
|
share/doc/coq/html/node.3.1.7.html
|
|
share/doc/coq/html/node.3.1.8.html
|
|
share/doc/coq/html/node.3.1.html
|
|
share/doc/coq/html/node.3.2.0.html
|
|
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.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.2.html
|
|
share/doc/coq/html/node.3.3.3.html
|
|
share/doc/coq/html/node.3.3.4.html
|
|
share/doc/coq/html/node.3.3.5.html
|
|
share/doc/coq/html/node.3.3.6.html
|
|
share/doc/coq/html/node.3.3.7.html
|
|
share/doc/coq/html/node.3.3.8.html
|
|
share/doc/coq/html/node.3.3.9.html
|
|
share/doc/coq/html/node.3.3.html
|
|
share/doc/coq/html/node.3.4.0.html
|
|
share/doc/coq/html/node.3.4.1.html
|
|
share/doc/coq/html/node.3.4.2.html
|
|
share/doc/coq/html/node.3.4.3.html
|
|
share/doc/coq/html/node.3.4.html
|
|
share/doc/coq/html/node.3.5.0.html
|
|
share/doc/coq/html/node.3.5.1.html
|
|
share/doc/coq/html/node.3.5.2.html
|
|
share/doc/coq/html/node.3.5.3.html
|
|
share/doc/coq/html/node.3.5.4.html
|
|
share/doc/coq/html/node.3.5.5.html
|
|
share/doc/coq/html/node.3.5.6.html
|
|
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.html
|
|
share/doc/coq/html/node.3.7.0.html
|
|
share/doc/coq/html/node.3.7.1.html
|
|
share/doc/coq/html/node.3.7.2.html
|
|
share/doc/coq/html/node.3.7.3.html
|
|
share/doc/coq/html/node.3.7.4.html
|
|
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.html
|
|
share/doc/coq/html/node.4.html
|
|
share/doc/coq/html/node.5.html
|
|
share/doc/coq/html/node.6.html
|
|
share/doc/coq/html/node.7.html
|
|
share/doc/coq/html/node.8.html
|
|
share/doc/coq/html/node.x.0.0.html
|
|
share/doc/coq/html/node.x.0.1.html
|
|
share/doc/coq/html/node.x.0.html
|
|
share/doc/coq/html/node.x.1.0.html
|
|
share/doc/coq/html/node.x.1.1.html
|
|
share/doc/coq/html/node.x.1.2.html
|
|
share/doc/coq/html/node.x.1.3.html
|
|
share/doc/coq/html/node.x.1.html
|
|
share/doc/coq/html/prev.gif
|
|
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/emacs/site-lisp/coq.el
|
|
@dirrm share/doc/coq/ps
|
|
@dirrm share/doc/coq/html
|
|
@dirrm share/doc/coq
|
|
@dirrm lib/coq/theories/ZArith
|
|
@dirrm lib/coq/theories/Wellfounded
|
|
@dirrm lib/coq/theories/Sets
|
|
@dirrm lib/coq/theories/Relations
|
|
@dirrm lib/coq/theories/Reals
|
|
@dirrm lib/coq/theories/Logic
|
|
@dirrm lib/coq/theories/Lists
|
|
@dirrm lib/coq/theories/IntMap
|
|
@dirrm lib/coq/theories/Init
|
|
@dirrm lib/coq/theories/Bool
|
|
@dirrm lib/coq/theories/Arith
|
|
@dirrm lib/coq/theories
|
|
@dirrm lib/coq/tactics
|
|
@dirrm lib/coq/states
|
|
@dirrm lib/coq/contrib/xml
|
|
@dirrm lib/coq/contrib/ring
|
|
@dirrm lib/coq/contrib/omega
|
|
@dirrm lib/coq/contrib/interface
|
|
@dirrm lib/coq/contrib/fourier
|
|
@dirrm lib/coq/contrib/field
|
|
@dirrm lib/coq/contrib/extraction
|
|
@dirrm lib/coq/contrib/correctness
|
|
@dirrm lib/coq/contrib
|
|
@dirrm lib/coq
|