Look up function:
FREE SOFTWARE ON CAMLCITY.ORG
Interactive proof assistant
From the coq web site: Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * to define functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to check these proofs by a relatively small certification "kernel".
| Version: | 8.1pl4godi2 |
| Homepage: | http://coq.inria.fr |
| Maintainer: | Virgile Prevosto <virgile.prevosto@m4x.org> |
| Files: |
bin/coq-interface bin/coq-interface.opt bin/coq-tex bin/coq_makefile bin/coqc bin/coqdep bin/coqdoc bin/coqide.byte bin/coqide.opt bin/coqmktop bin/coqtop.byte bin/coqtop.opt bin/coqwc bin/gallina bin/parser bin/parser.opt doc/apps-coq/COPYRIGHT doc/apps-coq/CREDITS doc/apps-coq/LICENSE lib/coq/acic.cmi lib/coq/acic.cmi_pretty lib/coq/acic2Xml.cmi lib/coq/acic2Xml.cmi_pretty lib/coq/auto.cmi lib/coq/auto.cmi_pretty lib/coq/autorewrite.cmi lib/coq/autorewrite.cmi_pretty lib/coq/bigint.cmi lib/coq/bigint.cmi_pretty lib/coq/bstack.cmi lib/coq/bstack.cmi_pretty lib/coq/btermdn.cmi lib/coq/btermdn.cmi_pretty lib/coq/cases.cmi lib/coq/cases.cmi_pretty lib/coq/cbv.cmi lib/coq/cbv.cmi_pretty lib/coq/cbytecodes.cmi lib/coq/cbytecodes.cmi_pretty lib/coq/cbytegen.cmi lib/coq/cbytegen.cmi_pretty lib/coq/ccalgo.cmi lib/coq/ccalgo.cmi_pretty lib/coq/ccproof.cmi lib/coq/ccproof.cmi_pretty lib/coq/cctac.cmi lib/coq/cctac.cmi_pretty lib/coq/cemitcodes.cmi lib/coq/cemitcodes.cmi_pretty lib/coq/cerrors.cmi lib/coq/cerrors.cmi_pretty lib/coq/cic2Xml.cmi lib/coq/cic2Xml.cmi_pretty lib/coq/cic2acic.cmi lib/coq/cic2acic.cmi_pretty lib/coq/class.cmi lib/coq/class.cmi_pretty lib/coq/classops.cmi lib/coq/classops.cmi_pretty lib/coq/clenv.cmi lib/coq/clenv.cmi_pretty lib/coq/clenvtac.cmi lib/coq/clenvtac.cmi_pretty lib/coq/closure.cmi lib/coq/closure.cmi_pretty lib/coq/coercion.cmi lib/coq/coercion.cmi_pretty lib/coq/command.cmi lib/coq/command.cmi_pretty lib/coq/common.cmi lib/coq/common.cmi_pretty lib/coq/compat.cmi lib/coq/compat.cmi_pretty lib/coq/const_omega.cmi lib/coq/const_omega.cmi_pretty lib/coq/constrextern.cmi lib/coq/constrextern.cmi_pretty lib/coq/constrintern.cmi lib/coq/constrintern.cmi_pretty lib/coq/contradiction.cmi lib/coq/contradiction.cmi_pretty lib/coq/contrib.cma lib/coq/contrib.cmxa 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/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_abstract.vo lib/coq/contrib/ring/Ring_normalize.vo lib/coq/contrib/ring/Setoid_ring.vo lib/coq/contrib/ring/Setoid_ring_normalize.vo lib/coq/contrib/ring/Setoid_ring_theory.vo lib/coq/contrib/romega/ROmega.vo lib/coq/contrib/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/Heq.vo lib/coq/contrib/subtac/Subtac.vo lib/coq/contrib/subtac/SubtacTactics.vo lib/coq/contrib/subtac/Utils.vo lib/coq/conv_oracle.cmi lib/coq/conv_oracle.cmi_pretty lib/coq/cooking.cmi lib/coq/cooking.cmi_pretty lib/coq/copcodes.cmi lib/coq/copcodes.cmi_pretty lib/coq/coq_config.cmi lib/coq/coq_config.cmi_pretty lib/coq/coq_omega.cmi lib/coq/coq_omega.cmi_pretty lib/coq/coqinit.cmi lib/coq/coqinit.cmi_pretty lib/coq/coqlib.cmi lib/coq/coqlib.cmi_pretty lib/coq/coqtop.cmi lib/coq/coqtop.cmi_pretty lib/coq/csymtable.cmi lib/coq/csymtable.cmi_pretty lib/coq/decl_interp.cmi lib/coq/decl_interp.cmi_pretty lib/coq/decl_kinds.cmi lib/coq/decl_kinds.cmi_pretty lib/coq/decl_mode.cmi lib/coq/decl_mode.cmi_pretty lib/coq/decl_proof_instr.cmi lib/coq/decl_proof_instr.cmi_pretty lib/coq/declarations.cmi lib/coq/declarations.cmi_pretty lib/coq/declare.cmi lib/coq/declare.cmi_pretty lib/coq/declaremods.cmi lib/coq/declaremods.cmi_pretty lib/coq/detyping.cmi lib/coq/detyping.cmi_pretty lib/coq/dhyp.cmi lib/coq/dhyp.cmi_pretty lib/coq/discharge.cmi lib/coq/discharge.cmi_pretty lib/coq/dischargedhypsmap.cmi lib/coq/dischargedhypsmap.cmi_pretty lib/coq/dn.cmi lib/coq/dn.cmi_pretty lib/coq/doubleTypeInference.cmi lib/coq/doubleTypeInference.cmi_pretty lib/coq/dp.cmi lib/coq/dp.cmi_pretty lib/coq/dp_why.cmi lib/coq/dp_why.cmi_pretty lib/coq/dyn.cmi lib/coq/dyn.cmi_pretty lib/coq/eauto.cmi lib/coq/eauto.cmi_pretty lib/coq/edit.cmi lib/coq/edit.cmi_pretty lib/coq/egrammar.cmi lib/coq/egrammar.cmi_pretty lib/coq/elim.cmi lib/coq/elim.cmi_pretty lib/coq/entries.cmi lib/coq/entries.cmi_pretty lib/coq/environ.cmi lib/coq/environ.cmi_pretty lib/coq/equality.cmi lib/coq/equality.cmi_pretty lib/coq/esubst.cmi lib/coq/esubst.cmi_pretty lib/coq/eterm.cmi lib/coq/eterm.cmi_pretty lib/coq/evar_refiner.cmi lib/coq/evar_refiner.cmi_pretty lib/coq/evar_tactics.cmi lib/coq/evar_tactics.cmi_pretty lib/coq/evarconv.cmi lib/coq/evarconv.cmi_pretty lib/coq/evarutil.cmi lib/coq/evarutil.cmi_pretty lib/coq/evd.cmi lib/coq/evd.cmi_pretty lib/coq/explore.cmi lib/coq/explore.cmi_pretty lib/coq/extend.cmi lib/coq/extend.cmi_pretty lib/coq/extraargs.cmi lib/coq/extraargs.cmi_pretty lib/coq/extract_env.cmi lib/coq/extract_env.cmi_pretty lib/coq/extraction.cmi lib/coq/extraction.cmi_pretty lib/coq/extratactics.cmi lib/coq/extratactics.cmi_pretty lib/coq/field.cmi lib/coq/field.cmi_pretty lib/coq/formula.cmi lib/coq/formula.cmi_pretty lib/coq/fourier.cmi lib/coq/fourier.cmi_pretty lib/coq/fourierR.cmi lib/coq/fourierR.cmi_pretty lib/coq/functional_principles_proofs.cmi lib/coq/functional_principles_proofs.cmi_pretty lib/coq/functional_principles_types.cmi lib/coq/functional_principles_types.cmi_pretty lib/coq/g_ascii_syntax.cmi lib/coq/g_ascii_syntax.cmi_pretty lib/coq/g_congruence.cmi lib/coq/g_congruence.cmi_pretty lib/coq/g_constr.cmi lib/coq/g_constr.cmi_pretty lib/coq/g_decl_mode.cmi lib/coq/g_decl_mode.cmi_pretty lib/coq/g_dp.cmi lib/coq/g_dp.cmi_pretty lib/coq/g_eterm.cmi lib/coq/g_eterm.cmi_pretty lib/coq/g_extraction.cmi lib/coq/g_extraction.cmi_pretty lib/coq/g_fourier.cmi lib/coq/g_fourier.cmi_pretty lib/coq/g_ground.cmi lib/coq/g_ground.cmi_pretty lib/coq/g_ltac.cmi lib/coq/g_ltac.cmi_pretty lib/coq/g_natsyntax.cmi lib/coq/g_natsyntax.cmi_pretty lib/coq/g_omega.cmi lib/coq/g_omega.cmi_pretty lib/coq/g_prim.cmi lib/coq/g_prim.cmi_pretty lib/coq/g_proofs.cmi lib/coq/g_proofs.cmi_pretty lib/coq/g_quote.cmi lib/coq/g_quote.cmi_pretty lib/coq/g_ring.cmi lib/coq/g_ring.cmi_pretty lib/coq/g_romega.cmi lib/coq/g_romega.cmi_pretty lib/coq/g_rsyntax.cmi lib/coq/g_rsyntax.cmi_pretty lib/coq/g_rtauto.cmi lib/coq/g_rtauto.cmi_pretty lib/coq/g_string_syntax.cmi lib/coq/g_string_syntax.cmi_pretty lib/coq/g_subtac.cmi lib/coq/g_subtac.cmi_pretty lib/coq/g_tactic.cmi lib/coq/g_tactic.cmi_pretty lib/coq/g_vernac.cmi lib/coq/g_vernac.cmi_pretty lib/coq/g_xml.cmi lib/coq/g_xml.cmi_pretty lib/coq/g_zsyntax.cmi lib/coq/g_zsyntax.cmi_pretty lib/coq/genarg.cmi lib/coq/genarg.cmi_pretty lib/coq/global.cmi lib/coq/global.cmi_pretty lib/coq/gmap.cmi lib/coq/gmap.cmi_pretty lib/coq/gmapl.cmi lib/coq/gmapl.cmi_pretty lib/coq/goptions.cmi lib/coq/goptions.cmi_pretty lib/coq/grammar.cma lib/coq/ground.cmi lib/coq/ground.cmi_pretty lib/coq/gset.cmi lib/coq/gset.cmi_pretty lib/coq/hashcons.cmi lib/coq/hashcons.cmi_pretty lib/coq/haskell.cmi lib/coq/haskell.cmi_pretty lib/coq/heap.cmi lib/coq/heap.cmi_pretty lib/coq/hiddentac.cmi lib/coq/hiddentac.cmi_pretty lib/coq/highparsing.cma lib/coq/highparsing.cmxa lib/coq/hightactics.cma lib/coq/hightactics.cmxa lib/coq/himsg.cmi lib/coq/himsg.cmi_pretty lib/coq/hipattern.cmi lib/coq/hipattern.cmi_pretty lib/coq/ide/.coqide-gtk2rc lib/coq/ide/FAQ lib/coq/ide/coq.png lib/coq/ide/utf8.v lib/coq/ide/utf8.vo lib/coq/impargs.cmi lib/coq/impargs.cmi_pretty lib/coq/indfun.cmi lib/coq/indfun.cmi_pretty lib/coq/indfun_common.cmi lib/coq/indfun_common.cmi_pretty lib/coq/indfun_main.cmi lib/coq/indfun_main.cmi_pretty lib/coq/indrec.cmi lib/coq/indrec.cmi_pretty lib/coq/indtypes.cmi lib/coq/indtypes.cmi_pretty lib/coq/inductive.cmi lib/coq/inductive.cmi_pretty lib/coq/inductiveops.cmi lib/coq/inductiveops.cmi_pretty lib/coq/instances.cmi lib/coq/instances.cmi_pretty lib/coq/interp.cma lib/coq/interp.cmxa lib/coq/inv.cmi lib/coq/inv.cmi_pretty lib/coq/invfun.cmi lib/coq/invfun.cmi_pretty lib/coq/jall.cmi lib/coq/jall.cmi_pretty lib/coq/jlogic.cmi lib/coq/jlogic.cmi_pretty lib/coq/jprover.cmi lib/coq/jprover.cmi_pretty lib/coq/jterm.cmi lib/coq/jterm.cmi_pretty lib/coq/jtunify.cmi lib/coq/jtunify.cmi_pretty lib/coq/kernel.cma lib/coq/kernel.cmxa lib/coq/leminv.cmi lib/coq/leminv.cmi_pretty lib/coq/lexer.cmi lib/coq/lexer.cmi_pretty lib/coq/lib.cma lib/coq/lib.cmi lib/coq/lib.cmi_pretty lib/coq/lib.cmxa lib/coq/libnames.cmi lib/coq/libnames.cmi_pretty lib/coq/libobject.cmi lib/coq/libobject.cmi_pretty lib/coq/library.cma lib/coq/library.cmi lib/coq/library.cmi_pretty lib/coq/library.cmxa lib/coq/line_oriented_parser.cmi lib/coq/line_oriented_parser.cmi_pretty lib/coq/logic.cmi lib/coq/logic.cmi_pretty lib/coq/matching.cmi lib/coq/matching.cmi_pretty lib/coq/merge.cmi lib/coq/merge.cmi_pretty lib/coq/metasyntax.cmi lib/coq/metasyntax.cmi_pretty lib/coq/mltop.cmi lib/coq/mltop.cmi_pretty lib/coq/mlutil.cmi lib/coq/mlutil.cmi_pretty lib/coq/mod_subst.cmi lib/coq/mod_subst.cmi_pretty lib/coq/mod_typing.cmi lib/coq/mod_typing.cmi_pretty lib/coq/modintern.cmi lib/coq/modintern.cmi_pretty lib/coq/modops.cmi lib/coq/modops.cmi_pretty lib/coq/modutil.cmi lib/coq/modutil.cmi_pretty lib/coq/nameops.cmi lib/coq/nameops.cmi_pretty lib/coq/names.cmi lib/coq/names.cmi_pretty lib/coq/nametab.cmi lib/coq/nametab.cmi_pretty lib/coq/nbtermdn.cmi lib/coq/nbtermdn.cmi_pretty lib/coq/newring.cmi lib/coq/newring.cmi_pretty lib/coq/notation.cmi lib/coq/notation.cmi_pretty lib/coq/ocaml.cmi lib/coq/ocaml.cmi_pretty lib/coq/omega.cmi lib/coq/omega.cmi_pretty lib/coq/opname.cmi lib/coq/opname.cmi_pretty lib/coq/options.cmi lib/coq/options.cmi_pretty lib/coq/parsing.cma lib/coq/parsing.cmxa lib/coq/pattern.cmi lib/coq/pattern.cmi_pretty lib/coq/pcoq.cmi lib/coq/pcoq.cmi_pretty lib/coq/pfedit.cmi lib/coq/pfedit.cmi_pretty lib/coq/pp.cmi lib/coq/pp.cmi_pretty lib/coq/pp_control.cmi lib/coq/pp_control.cmi_pretty lib/coq/ppconstr.cmi lib/coq/ppconstr.cmi_pretty lib/coq/ppdecl_proof.cmi lib/coq/ppdecl_proof.cmi_pretty lib/coq/ppextend.cmi lib/coq/ppextend.cmi_pretty lib/coq/pptactic.cmi lib/coq/pptactic.cmi_pretty lib/coq/ppvernac.cmi lib/coq/ppvernac.cmi_pretty lib/coq/pre_env.cmi lib/coq/pre_env.cmi_pretty lib/coq/predicate.cmi lib/coq/predicate.cmi_pretty lib/coq/prettyp.cmi lib/coq/prettyp.cmi_pretty lib/coq/pretype_errors.cmi lib/coq/pretype_errors.cmi_pretty lib/coq/pretyping.cma lib/coq/pretyping.cmi lib/coq/pretyping.cmi_pretty lib/coq/pretyping.cmxa lib/coq/printer.cmi lib/coq/printer.cmi_pretty lib/coq/printmod.cmi lib/coq/printmod.cmi_pretty lib/coq/profile.cmi lib/coq/profile.cmi_pretty lib/coq/proof2aproof.cmi lib/coq/proof2aproof.cmi_pretty lib/coq/proofTree2Xml.cmi lib/coq/proofTree2Xml.cmi_pretty lib/coq/proof_search.cmi lib/coq/proof_search.cmi_pretty lib/coq/proof_trees.cmi lib/coq/proof_trees.cmi_pretty lib/coq/proof_type.cmi lib/coq/proof_type.cmi_pretty lib/coq/proofs.cma lib/coq/proofs.cmxa lib/coq/protectedtoplevel.cmi lib/coq/protectedtoplevel.cmi_pretty lib/coq/quote.cmi lib/coq/quote.cmi_pretty lib/coq/rawterm.cmi lib/coq/rawterm.cmi_pretty lib/coq/rawterm_to_relation.cmi lib/coq/rawterm_to_relation.cmi_pretty lib/coq/rawtermops.cmi lib/coq/rawtermops.cmi_pretty lib/coq/recdef.cmi lib/coq/recdef.cmi_pretty lib/coq/record.cmi lib/coq/record.cmi_pretty lib/coq/recordops.cmi lib/coq/recordops.cmi_pretty lib/coq/redexpr.cmi lib/coq/redexpr.cmi_pretty lib/coq/reduction.cmi lib/coq/reduction.cmi_pretty lib/coq/reductionops.cmi lib/coq/reductionops.cmi_pretty lib/coq/refine.cmi lib/coq/refine.cmi_pretty lib/coq/refiner.cmi lib/coq/refiner.cmi_pretty lib/coq/refl_omega.cmi lib/coq/refl_omega.cmi_pretty lib/coq/refl_tauto.cmi lib/coq/refl_tauto.cmi_pretty lib/coq/reserve.cmi lib/coq/reserve.cmi_pretty lib/coq/retyping.cmi lib/coq/retyping.cmi_pretty lib/coq/ring.cmi lib/coq/ring.cmi_pretty lib/coq/rtree.cmi lib/coq/rtree.cmi_pretty lib/coq/rules.cmi lib/coq/rules.cmi_pretty lib/coq/safe_typing.cmi lib/coq/safe_typing.cmi_pretty lib/coq/scheme.cmi lib/coq/scheme.cmi_pretty lib/coq/search.cmi lib/coq/search.cmi_pretty lib/coq/sequent.cmi lib/coq/sequent.cmi_pretty lib/coq/setoid_replace.cmi lib/coq/setoid_replace.cmi_pretty lib/coq/sign.cmi lib/coq/sign.cmi_pretty lib/coq/states.cmi lib/coq/states.cmi_pretty lib/coq/states/initial.coq lib/coq/subtac.cmi lib/coq/subtac.cmi_pretty lib/coq/subtac_cases.cmi lib/coq/subtac_cases.cmi_pretty lib/coq/subtac_coercion.cmi lib/coq/subtac_coercion.cmi_pretty lib/coq/subtac_command.cmi lib/coq/subtac_command.cmi_pretty lib/coq/subtac_errors.cmi lib/coq/subtac_errors.cmi_pretty lib/coq/subtac_obligations.cmi lib/coq/subtac_obligations.cmi_pretty lib/coq/subtac_pretyping.cmi lib/coq/subtac_pretyping.cmi_pretty lib/coq/subtac_pretyping_F.cmi lib/coq/subtac_pretyping_F.cmi_pretty lib/coq/subtac_utils.cmi lib/coq/subtac_utils.cmi_pretty lib/coq/subtyping.cmi lib/coq/subtyping.cmi_pretty lib/coq/summary.cmi lib/coq/summary.cmi_pretty lib/coq/syntax_def.cmi lib/coq/syntax_def.cmi_pretty lib/coq/system.cmi lib/coq/system.cmi_pretty lib/coq/table.cmi lib/coq/table.cmi_pretty lib/coq/tacexpr.cmi lib/coq/tacexpr.cmi_pretty lib/coq/tacinterp.cmi lib/coq/tacinterp.cmi_pretty lib/coq/tacinv.cmi lib/coq/tacinv.cmi_pretty lib/coq/tacinvutils.cmi lib/coq/tacinvutils.cmi_pretty lib/coq/tacmach.cmi lib/coq/tacmach.cmi_pretty lib/coq/tacred.cmi lib/coq/tacred.cmi_pretty lib/coq/tactic_debug.cmi lib/coq/tactic_debug.cmi_pretty lib/coq/tactic_printer.cmi lib/coq/tactic_printer.cmi_pretty lib/coq/tacticals.cmi lib/coq/tacticals.cmi_pretty lib/coq/tactics.cma lib/coq/tactics.cmi lib/coq/tactics.cmi_pretty lib/coq/tactics.cmxa lib/coq/term.cmi lib/coq/term.cmi_pretty lib/coq/term_typing.cmi lib/coq/term_typing.cmi_pretty lib/coq/termdn.cmi lib/coq/termdn.cmi_pretty lib/coq/termops.cmi lib/coq/termops.cmi_pretty 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 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/Factorial.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 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/Bvector.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/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 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/Allmaps.vo lib/coq/theories/IntMap/Fset.vo lib/coq/theories/IntMap/Lsort.vo lib/coq/theories/IntMap/Map.vo lib/coq/theories/IntMap/Mapaxioms.vo lib/coq/theories/IntMap/Mapc.vo lib/coq/theories/IntMap/Mapcanon.vo lib/coq/theories/IntMap/Mapcard.vo lib/coq/theories/IntMap/Mapfold.vo lib/coq/theories/IntMap/Mapiter.vo lib/coq/theories/IntMap/Maplists.vo lib/coq/theories/IntMap/Mapsubset.vo lib/coq/theories/Lists/List.vo lib/coq/theories/Lists/ListSet.vo lib/coq/theories/Lists/ListTactics.vo lib/coq/theories/Lists/MonoList.vo lib/coq/theories/Lists/SetoidList.vo lib/coq/theories/Lists/Streams.vo lib/coq/theories/Lists/TheoryList.vo lib/coq/theories/Logic/Berardi.vo 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 lib/coq/theories/Reals/Binomial.vo lib/coq/theories/Reals/Cauchy_prod.vo lib/coq/theories/Reals/Cos_plus.vo 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 lib/coq/theories/Reals/PartSum.vo lib/coq/theories/Reals/RIneq.vo lib/coq/theories/Reals/RList.vo lib/coq/theories/Reals/R_Ifp.vo lib/coq/theories/Reals/R_sqr.vo lib/coq/theories/Reals/R_sqrt.vo lib/coq/theories/Reals/Ranalysis.vo lib/coq/theories/Reals/Ranalysis1.vo lib/coq/theories/Reals/Ranalysis2.vo lib/coq/theories/Reals/Ranalysis3.vo lib/coq/theories/Reals/Ranalysis4.vo lib/coq/theories/Reals/Raxioms.vo lib/coq/theories/Reals/Rbase.vo lib/coq/theories/Reals/Rbasic_fun.vo lib/coq/theories/Reals/Rcomplete.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/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 lib/coq/theories/Reals/Rsigma.vo lib/coq/theories/Reals/Rsqrt_def.vo lib/coq/theories/Reals/Rtopology.vo lib/coq/theories/Reals/Rtrigo.vo lib/coq/theories/Reals/Rtrigo_alt.vo lib/coq/theories/Reals/Rtrigo_calc.vo lib/coq/theories/Reals/Rtrigo_def.vo lib/coq/theories/Reals/Rtrigo_fun.vo lib/coq/theories/Reals/Rtrigo_reg.vo lib/coq/theories/Reals/SeqProp.vo lib/coq/theories/Reals/SeqSeries.vo lib/coq/theories/Reals/SplitAbsolu.vo lib/coq/theories/Reals/SplitRmult.vo lib/coq/theories/Reals/Sqrt_reg.vo lib/coq/theories/Relations/Newman.vo lib/coq/theories/Relations/Operators_Properties.vo lib/coq/theories/Relations/Relation_Definitions.vo lib/coq/theories/Relations/Relation_Operators.vo lib/coq/theories/Relations/Relations.vo lib/coq/theories/Relations/Rstar.vo lib/coq/theories/Setoids/Setoid.vo lib/coq/theories/Sets/Classical_sets.vo lib/coq/theories/Sets/Constructive_sets.vo 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/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 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/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 lib/coq/theories/ZArith/ZArith_dec.vo lib/coq/theories/ZArith/Zabs.vo lib/coq/theories/ZArith/Zbinary.vo lib/coq/theories/ZArith/Zbool.vo lib/coq/theories/ZArith/Zcompare.vo lib/coq/theories/ZArith/Zcomplements.vo lib/coq/theories/ZArith/Zdiv.vo lib/coq/theories/ZArith/Zeven.vo lib/coq/theories/ZArith/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/tlm.cmi lib/coq/tlm.cmi_pretty lib/coq/tools/coqdoc/coqdoc.css lib/coq/tools/coqdoc/coqdoc.sty lib/coq/topconstr.cmi lib/coq/topconstr.cmi_pretty lib/coq/toplevel.cma lib/coq/toplevel.cmi lib/coq/toplevel.cmi_pretty lib/coq/toplevel.cmxa lib/coq/type_errors.cmi lib/coq/type_errors.cmi_pretty lib/coq/typeops.cmi lib/coq/typeops.cmi_pretty lib/coq/typing.cmi lib/coq/typing.cmi_pretty lib/coq/unification.cmi lib/coq/unification.cmi_pretty lib/coq/unify.cmi lib/coq/unify.cmi_pretty lib/coq/univ.cmi lib/coq/univ.cmi_pretty lib/coq/unshare.cmi lib/coq/unshare.cmi_pretty lib/coq/usage.cmi lib/coq/usage.cmi_pretty lib/coq/util.cmi lib/coq/util.cmi_pretty lib/coq/vconv.cmi lib/coq/vconv.cmi_pretty lib/coq/vernac.cmi lib/coq/vernac.cmi_pretty lib/coq/vernacentries.cmi lib/coq/vernacentries.cmi_pretty lib/coq/vernacexpr.cmi lib/coq/vernacexpr.cmi_pretty lib/coq/vernacinterp.cmi lib/coq/vernacinterp.cmi_pretty lib/coq/vm.cmi lib/coq/vm.cmi_pretty lib/coq/vnorm.cmi lib/coq/vnorm.cmi_pretty lib/coq/whelp.cmi lib/coq/whelp.cmi_pretty lib/coq/xml.cmi lib/coq/xml.cmi_pretty lib/coq/xmlcommand.cmi lib/coq/xmlcommand.cmi_pretty lib/coq/xmlentries.cmi lib/coq/xmlentries.cmi_pretty man/man1/coq-interface.1.html man/man1/coq-tex.1.html man/man1/coq_makefile.1.html man/man1/coqc.1.html man/man1/coqdep.1.html man/man1/coqdoc.1.html man/man1/coqmktop.1.html man/man1/coqtop.1.html man/man1/coqtop.byte.1.html man/man1/coqtop.opt.1.html man/man1/coqwc.1.html man/man1/gallina.1.html man/man1/parser.1.html share/emacs/site-lisp/coq-inferior.el share/emacs/site-lisp/coq.el share/texmf/tex/latex/misc/coqdoc.sty |
| Built from sources: |
coq-8.1pl4 |
