Skip to content

Instantly share code, notes, and snippets.

@kennknowles

kennknowles/gist:3515580

Created August 29, 2012 16:54
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save kennknowles/3515580 to your computer and use it in GitHub Desktop.
Save kennknowles/3515580 to your computer and use it in GitHub Desktop.
Download ZIP
brew install coq
Raw
gistfile1.txt
==> Downloading http://coq.inria.fr/distrib/V8.4/files/coq-8.4.tar.gz
Already downloaded: /Users/kenn/Library/Caches/Homebrew/coq-8.4.tar.gz
/usr/bin/tar xf /Users/kenn/Library/Caches/Homebrew/coq-8.4.tar.gz
==> ./configure -prefix /usr/local/Cellar/coq/8.4 -mandir /usr/local/Cellar/coq/8.4/share/man -camlp5dir /usr/local/Cellar/camlp5/6.06/lib/ocaml/camlp5 -emacslib /usr/local/Cellar/coq/8.4/lib/emacs/site-lisp -coqdocdir /usr/local/Cellar/coq/8.4/share/coq/latex -coqide no -with-doc no -arch x86_64
./configure -prefix /usr/local/Cellar/coq/8.4 -mandir /usr/local/Cellar/coq/8.4/share/man -camlp5dir /usr/local/Cellar/camlp5/6.06/lib/ocaml/camlp5 -emacslib /usr/local/Cellar/coq/8.4/lib/emacs/site-lisp -coqdocdir /usr/local/Cellar/coq/8.4/share/coq/latex -coqide no -with-doc no -arch x86_64
You have GNU Make 3.81. Good!
You have Objective-Caml 4.00.0. Good!
You have native-code compilation. Good!
CoqIde disabled as requested.
Coq top directory : /private/tmp/homebrew-coq-8.4-dzw8/coq-8.4
Architecture : x86_64
Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/usr/local/Cellar/coq/8.4/lib/coq'
Coq tools bytecode link flags :
OS dependent libraries : -cclib -lunix
Objective-Caml/Camlp4 version : 4.00.0
Objective-Caml/Camlp4 binaries in : /usr/local/bin
Objective-Caml library in : /usr/local/lib/ocaml
Camlp4 library in : /usr/local/Cellar/camlp5/6.06/lib/ocaml/camlp5
Native dynamic link support : true
Documentation : None
CoqIde : no
Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
Coq web site : http://coq.inria.fr/
Paths for true installation:
binaries will be copied in /usr/local/Cellar/coq/8.4/bin
library will be copied in /usr/local/Cellar/coq/8.4/lib/coq
config files will be copied in /usr/local/Cellar/coq/8.4/etc/xdg/coq
data files will be copied in /usr/local/Cellar/coq/8.4/share/coq
man pages will be copied in /usr/local/Cellar/coq/8.4/share/man
documentation will be copied in /usr/local/Cellar/coq/8.4/share/doc/coq
emacs mode will be copied in /usr/local/Cellar/coq/8.4/lib/emacs/site-lisp
If anything in the above is wrong, please restart './configure'.
*Warning* To compile the system for a new architecture
don't forget to do a 'make archclean' before './configure'.
==> make world
make world
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
OCAMLLEX tools/coqdep_lexer.mll
348 states, 7127 transitions, table size 30596 bytes
3131 additional bytes used for bindings
OCAMLBEST -o bin/coqdep_boot
"ocaml" theories/Numbers/Natural/BigN/NMake_gen.ml > "theories/Numbers/Natural/BigN/NMake_gen.v" || (RV=$?; rm -f "theories/Numbers/Natural/BigN/NMake_gen.v"; exit ${RV})
COQDEP plugins/extraction/ExtrOcamlString.v
COQDEP plugins/extraction/ExtrOcamlZBigInt.v
COQDEP plugins/extraction/ExtrOcamlZInt.v
COQDEP plugins/extraction/ExtrOcamlNatBigInt.v
COQDEP plugins/extraction/ExtrOcamlNatInt.v
COQDEP plugins/extraction/ExtrOcamlBigIntConv.v
COQDEP plugins/extraction/ExtrOcamlIntConv.v
COQDEP plugins/extraction/ExtrOcamlBasic.v
COQDEP plugins/nsatz/Nsatz.v
COQDEP plugins/quote/Quote.v
COQDEP plugins/setoid_ring/Integral_domain.v
COQDEP plugins/setoid_ring/Rings_Q.v
COQDEP plugins/setoid_ring/Rings_R.v
COQDEP plugins/setoid_ring/Rings_Z.v
COQDEP plugins/setoid_ring/Ncring_tac.v
COQDEP plugins/setoid_ring/Ncring_initial.v
COQDEP plugins/setoid_ring/Ncring_polynom.v
COQDEP plugins/setoid_ring/Ncring.v
COQDEP plugins/setoid_ring/Cring.v
COQDEP plugins/setoid_ring/Algebra_syntax.v
COQDEP plugins/setoid_ring/ZArithRing.v
COQDEP plugins/setoid_ring/Ring.v
COQDEP plugins/setoid_ring/Ring_theory.v
COQDEP plugins/setoid_ring/Ring_tac.v
COQDEP plugins/setoid_ring/Ring_polynom.v
COQDEP plugins/setoid_ring/Ring_equiv.v
COQDEP plugins/setoid_ring/Ring_base.v
COQDEP plugins/setoid_ring/RealField.v
COQDEP plugins/setoid_ring/NArithRing.v
COQDEP plugins/setoid_ring/InitialRing.v
COQDEP plugins/setoid_ring/Field.v
COQDEP plugins/setoid_ring/Field_theory.v
COQDEP plugins/setoid_ring/Field_tac.v
COQDEP plugins/setoid_ring/BinList.v
COQDEP plugins/setoid_ring/ArithRing.v
COQDEP plugins/rtauto/Rtauto.v
COQDEP plugins/rtauto/Bintree.v
COQDEP plugins/funind/Recdef.v
COQDEP plugins/fourier/Fourier.v
COQDEP plugins/fourier/Fourier_util.v
COQDEP plugins/field/LegacyField.v
COQDEP plugins/field/LegacyField_Theory.v
COQDEP plugins/field/LegacyField_Tactic.v
COQDEP plugins/field/LegacyField_Compl.v
COQDEP plugins/ring/Setoid_ring.v
COQDEP plugins/ring/Setoid_ring_theory.v
COQDEP plugins/ring/Setoid_ring_normalize.v
COQDEP plugins/ring/Ring_normalize.v
COQDEP plugins/ring/Ring_abstract.v
COQDEP plugins/ring/LegacyZArithRing.v
COQDEP plugins/ring/LegacyRing.v
COQDEP plugins/ring/LegacyRing_theory.v
COQDEP plugins/ring/LegacyNArithRing.v
COQDEP plugins/ring/LegacyArithRing.v
COQDEP plugins/micromega/ZMicromega.v
COQDEP plugins/micromega/ZCoeff.v
COQDEP plugins/micromega/VarMap.v
COQDEP plugins/micromega/Tauto.v
COQDEP plugins/micromega/RMicromega.v
COQDEP plugins/micromega/RingMicromega.v
COQDEP plugins/micromega/Refl.v
COQDEP plugins/micromega/QMicromega.v
COQDEP plugins/micromega/Psatz.v
COQDEP plugins/micromega/OrderedRing.v
COQDEP plugins/micromega/Env.v
COQDEP plugins/micromega/EnvRing.v
COQDEP plugins/micromega/CheckerMaker.v
COQDEP plugins/romega/ROmega.v
COQDEP plugins/romega/ReflOmegaCore.v
COQDEP plugins/omega/PreOmega.v
COQDEP plugins/omega/Omega.v
COQDEP plugins/omega/OmegaPlugin.v
COQDEP plugins/omega/OmegaLemmas.v
COQDEP theories/Vectors/Vector.v
COQDEP theories/Vectors/VectorSpec.v
COQDEP theories/Vectors/VectorDef.v
COQDEP theories/Vectors/Fin.v
COQDEP theories/Structures/OrderedType.v
COQDEP theories/Structures/OrderedTypeEx.v
COQDEP theories/Structures/OrderedTypeAlt.v
COQDEP theories/Structures/DecidableTypeEx.v
COQDEP theories/Structures/DecidableType.v
COQDEP theories/Structures/GenericMinMax.v
COQDEP theories/Structures/OrdersAlt.v
COQDEP theories/Structures/OrdersTac.v
COQDEP theories/Structures/OrdersLists.v
COQDEP theories/Structures/OrdersFacts.v
COQDEP theories/Structures/OrdersEx.v
COQDEP theories/Structures/Orders.v
COQDEP theories/Structures/EqualitiesFacts.v
COQDEP theories/Structures/Equalities.v
COQDEP theories/Program/Wf.v
COQDEP theories/Program/Utils.v
COQDEP theories/Program/Tactics.v
COQDEP theories/Program/Syntax.v
COQDEP theories/Program/Subset.v
COQDEP theories/Program/Program.v
COQDEP theories/Program/Equality.v
COQDEP theories/Program/Combinators.v
COQDEP theories/Program/Basics.v
COQDEP theories/Classes/RelationPairs.v
COQDEP theories/Classes/SetoidTactics.v
COQDEP theories/Classes/SetoidDec.v
COQDEP theories/Classes/SetoidClass.v
COQDEP theories/Classes/RelationClasses.v
COQDEP theories/Classes/Morphisms.v
COQDEP theories/Classes/Morphisms_Relations.v
COQDEP theories/Classes/Morphisms_Prop.v
COQDEP theories/Classes/Init.v
COQDEP theories/Classes/EquivDec.v
COQDEP theories/Classes/Equivalence.v
COQDEP theories/Unicode/Utf8_core.v
COQDEP theories/Unicode/Utf8.v
COQDEP theories/Numbers/Rational/SpecViaQ/QSig.v
COQDEP theories/Numbers/Rational/BigQ/QMake.v
COQDEP theories/Numbers/Rational/BigQ/BigQ.v
COQDEP theories/Numbers/NumPrelude.v
COQDEP theories/Numbers/Natural/SpecViaZ/NSig.v
COQDEP theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
COQDEP theories/Numbers/Natural/Peano/NPeano.v
COQDEP theories/Numbers/Natural/Binary/NBinary.v
COQDEP theories/Numbers/Natural/BigN/NMake.v
COQDEP theories/Numbers/Natural/BigN/NMake_gen.v
COQDEP theories/Numbers/Natural/BigN/Nbasic.v
COQDEP theories/Numbers/Natural/BigN/BigN.v
COQDEP theories/Numbers/Natural/Abstract/NBits.v
COQDEP theories/Numbers/Natural/Abstract/NLcm.v
COQDEP theories/Numbers/Natural/Abstract/NGcd.v
COQDEP theories/Numbers/Natural/Abstract/NLog.v
COQDEP theories/Numbers/Natural/Abstract/NSqrt.v
COQDEP theories/Numbers/Natural/Abstract/NPow.v
COQDEP theories/Numbers/Natural/Abstract/NParity.v
COQDEP theories/Numbers/Natural/Abstract/NMaxMin.v
COQDEP theories/Numbers/Natural/Abstract/NDiv.v
COQDEP theories/Numbers/Natural/Abstract/NProperties.v
COQDEP theories/Numbers/Natural/Abstract/NSub.v
COQDEP theories/Numbers/Natural/Abstract/NStrongRec.v
COQDEP theories/Numbers/Natural/Abstract/NOrder.v
COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v
COQDEP theories/Numbers/Natural/Abstract/NIso.v
COQDEP theories/Numbers/Natural/Abstract/NDefOps.v
COQDEP theories/Numbers/Natural/Abstract/NBase.v
COQDEP theories/Numbers/Natural/Abstract/NAxioms.v
COQDEP theories/Numbers/Natural/Abstract/NAdd.v
COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v
COQDEP theories/Numbers/NatInt/NZBits.v
COQDEP theories/Numbers/NatInt/NZGcd.v
COQDEP theories/Numbers/NatInt/NZLog.v
COQDEP theories/Numbers/NatInt/NZSqrt.v
COQDEP theories/Numbers/NatInt/NZPow.v
COQDEP theories/Numbers/NatInt/NZDiv.v
COQDEP theories/Numbers/NatInt/NZParity.v
COQDEP theories/Numbers/NatInt/NZDomain.v
COQDEP theories/Numbers/NatInt/NZProperties.v
COQDEP theories/Numbers/NatInt/NZOrder.v
COQDEP theories/Numbers/NatInt/NZMul.v
COQDEP theories/Numbers/NatInt/NZMulOrder.v
COQDEP theories/Numbers/NatInt/NZBase.v
COQDEP theories/Numbers/NatInt/NZAxioms.v
COQDEP theories/Numbers/NatInt/NZAdd.v
COQDEP theories/Numbers/NatInt/NZAddOrder.v
COQDEP theories/Numbers/NaryFunctions.v
COQDEP theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
COQDEP theories/Numbers/Integer/SpecViaZ/ZSig.v
COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v
COQDEP theories/Numbers/Integer/Binary/ZBinary.v
COQDEP theories/Numbers/Integer/BigZ/ZMake.v
COQDEP theories/Numbers/Integer/BigZ/BigZ.v
COQDEP theories/Numbers/Integer/Abstract/ZProperties.v
COQDEP theories/Numbers/Integer/Abstract/ZBits.v
COQDEP theories/Numbers/Integer/Abstract/ZLcm.v
COQDEP theories/Numbers/Integer/Abstract/ZGcd.v
COQDEP theories/Numbers/Integer/Abstract/ZPow.v
COQDEP theories/Numbers/Integer/Abstract/ZParity.v
COQDEP theories/Numbers/Integer/Abstract/ZMaxMin.v
COQDEP theories/Numbers/Integer/Abstract/ZDivEucl.v
COQDEP theories/Numbers/Integer/Abstract/ZDivTrunc.v
COQDEP theories/Numbers/Integer/Abstract/ZDivFloor.v
COQDEP theories/Numbers/Integer/Abstract/ZSgnAbs.v
COQDEP theories/Numbers/Integer/Abstract/ZMul.v
COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v
COQDEP theories/Numbers/Integer/Abstract/ZLt.v
COQDEP theories/Numbers/Integer/Abstract/ZBase.v
COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v
COQDEP theories/Numbers/Integer/Abstract/ZAdd.v
COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v
COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v
COQDEP theories/Numbers/Cyclic/Int31/Ring31.v
COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v
COQDEP theories/Numbers/Cyclic/Int31/Int31.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v
COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
COQDEP theories/Numbers/BigNumPrelude.v
COQDEP theories/Numbers/BinNums.v
COQDEP theories/QArith/Qminmax.v
COQDEP theories/QArith/QOrderedType.v
COQDEP theories/QArith/Qround.v
COQDEP theories/QArith/Qring.v
COQDEP theories/QArith/Qreduction.v
COQDEP theories/QArith/Qreals.v
COQDEP theories/QArith/Qpower.v
COQDEP theories/QArith/Qfield.v
COQDEP theories/QArith/Qcanon.v
COQDEP theories/QArith/QArith.v
COQDEP theories/QArith/QArith_base.v
COQDEP theories/QArith/Qabs.v
COQDEP theories/Sorting/Mergesort.v
COQDEP theories/Sorting/Sorting.v
COQDEP theories/Sorting/Sorted.v
COQDEP theories/Sorting/PermutEq.v
COQDEP theories/Sorting/PermutSetoid.v
COQDEP theories/Sorting/Permutation.v
COQDEP theories/Sorting/Heap.v
COQDEP theories/Reals/Rminmax.v
COQDEP theories/Reals/ROrderedType.v
COQDEP theories/Reals/Sqrt_reg.v
COQDEP theories/Reals/SplitRmult.v
COQDEP theories/Reals/SplitAbsolu.v
COQDEP theories/Reals/SeqSeries.v
COQDEP theories/Reals/SeqProp.v
COQDEP theories/Reals/Rtrigo.v
COQDEP theories/Reals/Rtrigo1.v
COQDEP theories/Reals/Rtrigo_reg.v
COQDEP theories/Reals/Rtrigo_fun.v
COQDEP theories/Reals/Rtrigo_def.v
COQDEP theories/Reals/Rtrigo_calc.v
COQDEP theories/Reals/Rtrigo_alt.v
COQDEP theories/Reals/Rtopology.v
COQDEP theories/Reals/R_sqr.v
COQDEP theories/Reals/R_sqrt.v
COQDEP theories/Reals/Rsqrt_def.v
COQDEP theories/Reals/Rsigma.v
COQDEP theories/Reals/Rseries.v
COQDEP theories/Reals/Rprod.v
COQDEP theories/Reals/Rpower.v
COQDEP theories/Reals/Rpow_def.v
COQDEP theories/Reals/Rlogic.v
COQDEP theories/Reals/RList.v
COQDEP theories/Reals/Rlimit.v
COQDEP theories/Reals/RIneq.v
COQDEP theories/Reals/R_Ifp.v
COQDEP theories/Reals/RiemannInt.v
COQDEP theories/Reals/RiemannInt_SF.v
COQDEP theories/Reals/Rgeom.v
COQDEP theories/Reals/Rfunctions.v
COQDEP theories/Reals/Reals.v
COQDEP theories/Reals/Rderiv.v
COQDEP theories/Reals/Rdefinitions.v
COQDEP theories/Reals/Rcomplete.v
COQDEP theories/Reals/Rbasic_fun.v
COQDEP theories/Reals/Rbase.v
COQDEP theories/Reals/Raxioms.v
COQDEP theories/Reals/Ratan.v
COQDEP theories/Reals/Ranalysis_reg.v
COQDEP theories/Reals/Ranalysis.v
COQDEP theories/Reals/Ranalysis5.v
COQDEP theories/Reals/Ranalysis4.v
COQDEP theories/Reals/Ranalysis3.v
COQDEP theories/Reals/Ranalysis2.v
COQDEP theories/Reals/Ranalysis1.v
COQDEP theories/Reals/PSeries_reg.v
COQDEP theories/Reals/PartSum.v
COQDEP theories/Reals/NewtonInt.v
COQDEP theories/Reals/MVT.v
COQDEP theories/Reals/Machin.v
COQDEP theories/Reals/LegacyRfield.v
COQDEP theories/Reals/Integration.v
COQDEP theories/Reals/Exp_prop.v
COQDEP theories/Reals/DiscrR.v
COQDEP theories/Reals/Cos_rel.v
COQDEP theories/Reals/Cos_plus.v
COQDEP theories/Reals/Cauchy_prod.v
COQDEP theories/Reals/Binomial.v
COQDEP theories/Reals/ArithProp.v
COQDEP theories/Reals/AltSeries.v
COQDEP theories/Reals/Alembert.v
COQDEP theories/Wellfounded/Well_Ordering.v
COQDEP theories/Wellfounded/Wellfounded.v
COQDEP theories/Wellfounded/Union.v
COQDEP theories/Wellfounded/Transitive_Closure.v
COQDEP theories/Wellfounded/Lexicographic_Product.v
COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v
COQDEP theories/Wellfounded/Inverse_Image.v
COQDEP theories/Wellfounded/Inclusion.v
COQDEP theories/Wellfounded/Disjoint_Union.v
COQDEP theories/Relations/Relations.v
COQDEP theories/Relations/Relation_Operators.v
COQDEP theories/Relations/Relation_Definitions.v
COQDEP theories/Relations/Operators_Properties.v
COQDEP theories/MSets/MSetPositive.v
COQDEP theories/MSets/MSetWeakList.v
COQDEP theories/MSets/MSetToFiniteSet.v
COQDEP theories/MSets/MSets.v
COQDEP theories/MSets/MSetProperties.v
COQDEP theories/MSets/MSetList.v
COQDEP theories/MSets/MSetInterface.v
COQDEP theories/MSets/MSetFacts.v
COQDEP theories/MSets/MSetEqProperties.v
COQDEP theories/MSets/MSetDecide.v
COQDEP theories/MSets/MSetRBT.v
COQDEP theories/MSets/MSetAVL.v
COQDEP theories/MSets/MSetGenTree.v
COQDEP theories/FSets/FSetWeakList.v
COQDEP theories/FSets/FSetToFiniteSet.v
COQDEP theories/FSets/FSets.v
COQDEP theories/FSets/FSetProperties.v
COQDEP theories/FSets/FSetList.v
COQDEP theories/FSets/FSetInterface.v
COQDEP theories/FSets/FSetFacts.v
COQDEP theories/FSets/FSetEqProperties.v
COQDEP theories/FSets/FSetDecide.v
COQDEP theories/FSets/FSetBridge.v
COQDEP theories/FSets/FSetPositive.v
COQDEP theories/FSets/FSetAVL.v
COQDEP theories/FSets/FSetCompat.v
COQDEP theories/FSets/FMapWeakList.v
COQDEP theories/FSets/FMaps.v
COQDEP theories/FSets/FMapPositive.v
COQDEP theories/FSets/FMapList.v
COQDEP theories/FSets/FMapInterface.v
COQDEP theories/FSets/FMapFullAVL.v
COQDEP theories/FSets/FMapFacts.v
COQDEP theories/FSets/FMapAVL.v
COQDEP theories/Sets/Uniset.v
COQDEP theories/Sets/Relations_3.v
COQDEP theories/Sets/Relations_3_facts.v
COQDEP theories/Sets/Relations_2.v
COQDEP theories/Sets/Relations_2_facts.v
COQDEP theories/Sets/Relations_1.v
COQDEP theories/Sets/Relations_1_facts.v
COQDEP theories/Sets/Powerset.v
COQDEP theories/Sets/Powerset_facts.v
COQDEP theories/Sets/Powerset_Classical_facts.v
COQDEP theories/Sets/Permut.v
COQDEP theories/Sets/Partial_Order.v
COQDEP theories/Sets/Multiset.v
COQDEP theories/Sets/Integers.v
COQDEP theories/Sets/Infinite_sets.v
COQDEP theories/Sets/Image.v
COQDEP theories/Sets/Finite_sets.v
COQDEP theories/Sets/Finite_sets_facts.v
COQDEP theories/Sets/Ensembles.v
COQDEP theories/Sets/Cpo.v
COQDEP theories/Sets/Constructive_sets.v
COQDEP theories/Sets/Classical_sets.v
COQDEP theories/Strings/String.v
COQDEP theories/Strings/Ascii.v
COQDEP theories/Lists/Streams.v
COQDEP theories/Lists/StreamMemo.v
COQDEP theories/Lists/SetoidPermutation.v
COQDEP theories/Lists/SetoidList.v
COQDEP theories/Lists/List.v
COQDEP theories/Lists/ListTactics.v
COQDEP theories/Lists/ListSet.v
COQDEP theories/Setoids/Setoid.v
COQDEP theories/ZArith/Zeuclid.v
COQDEP theories/ZArith/Zwf.v
COQDEP theories/ZArith/Zsqrt_compat.v
COQDEP theories/ZArith/Zpow_facts.v
COQDEP theories/ZArith/Zpower.v
COQDEP theories/ZArith/Zpow_def.v
COQDEP theories/ZArith/Zorder.v
COQDEP theories/ZArith/Zquot.v
COQDEP theories/ZArith/ZOdiv.v
COQDEP theories/ZArith/ZOdiv_def.v
COQDEP theories/ZArith/Znumtheory.v
COQDEP theories/ZArith/Znat.v
COQDEP theories/ZArith/Zmisc.v
COQDEP theories/ZArith/Zmin.v
COQDEP theories/ZArith/Zminmax.v
COQDEP theories/ZArith/Zmax.v
COQDEP theories/ZArith/Zlogarithm.v
COQDEP theories/ZArith/Zhints.v
COQDEP theories/ZArith/Zpow_alt.v
COQDEP theories/ZArith/Zgcd_alt.v
COQDEP theories/ZArith/Zeven.v
COQDEP theories/ZArith/Zdiv.v
COQDEP theories/ZArith/Zcomplements.v
COQDEP theories/ZArith/Zcompare.v
COQDEP theories/ZArith/Zbool.v
COQDEP theories/ZArith/Zdigits.v
COQDEP theories/ZArith/ZArith.v
COQDEP theories/ZArith/ZArith_dec.v
COQDEP theories/ZArith/ZArith_base.v
COQDEP theories/ZArith/Zabs.v
COQDEP theories/ZArith/Wf_Z.v
COQDEP theories/ZArith/Int.v
COQDEP theories/ZArith/BinInt.v
COQDEP theories/ZArith/BinIntDef.v
COQDEP theories/ZArith/auxiliary.v
COQDEP theories/NArith/Ngcd_def.v
COQDEP theories/NArith/Nsqrt_def.v
COQDEP theories/NArith/Ndiv_def.v
COQDEP theories/NArith/Nnat.v
COQDEP theories/NArith/Ndist.v
COQDEP theories/NArith/Ndigits.v
COQDEP theories/NArith/Ndec.v
COQDEP theories/NArith/NArith.v
COQDEP theories/NArith/BinNat.v
COQDEP theories/NArith/BinNatDef.v
COQDEP theories/PArith/PArith.v
COQDEP theories/PArith/POrderedType.v
COQDEP theories/PArith/Pnat.v
COQDEP theories/PArith/BinPos.v
COQDEP theories/PArith/BinPosDef.v
COQDEP theories/Bool/Zerob.v
COQDEP theories/Bool/Sumbool.v
COQDEP theories/Bool/IfProp.v
COQDEP theories/Bool/DecBool.v
COQDEP theories/Bool/Bvector.v
COQDEP theories/Bool/Bool.v
COQDEP theories/Bool/BoolEq.v
COQDEP theories/Arith/Wf_nat.v
COQDEP theories/Arith/Plus.v
COQDEP theories/Arith/Peano_dec.v
COQDEP theories/Arith/Mult.v
COQDEP theories/Arith/Min.v
COQDEP theories/Arith/Minus.v
COQDEP theories/Arith/Max.v
COQDEP theories/Arith/Lt.v
COQDEP theories/Arith/Le.v
COQDEP theories/Arith/Gt.v
COQDEP theories/Arith/Factorial.v
COQDEP theories/Arith/Even.v
COQDEP theories/Arith/Euclid.v
COQDEP theories/Arith/EqNat.v
COQDEP theories/Arith/Div2.v
COQDEP theories/Arith/Compare.v
COQDEP theories/Arith/Compare_dec.v
COQDEP theories/Arith/Bool_nat.v
COQDEP theories/Arith/Between.v
COQDEP theories/Arith/Arith.v
COQDEP theories/Arith/Arith_base.v
COQDEP theories/Logic/SetIsType.v
COQDEP theories/Logic/RelationalChoice.v
COQDEP theories/Logic/ProofIrrelevance.v
COQDEP theories/Logic/ProofIrrelevanceFacts.v
COQDEP theories/Logic/JMeq.v
COQDEP theories/Logic/IndefiniteDescription.v
COQDEP theories/Logic/Hurkens.v
COQDEP theories/Logic/FunctionalExtensionality.v
COQDEP theories/Logic/Eqdep.v
COQDEP theories/Logic/EqdepFacts.v
COQDEP theories/Logic/Eqdep_dec.v
COQDEP theories/Logic/Epsilon.v
COQDEP theories/Logic/Diaconescu.v
COQDEP theories/Logic/Description.v
COQDEP theories/Logic/Decidable.v
COQDEP theories/Logic/ConstructiveEpsilon.v
COQDEP theories/Logic/Classical.v
COQDEP theories/Logic/ClassicalUniqueChoice.v
COQDEP theories/Logic/Classical_Type.v
COQDEP theories/Logic/Classical_Prop.v
COQDEP theories/Logic/Classical_Pred_Type.v
COQDEP theories/Logic/Classical_Pred_Set.v
COQDEP theories/Logic/ClassicalFacts.v
COQDEP theories/Logic/ClassicalEpsilon.v
COQDEP theories/Logic/ClassicalDescription.v
COQDEP theories/Logic/ClassicalChoice.v
COQDEP theories/Logic/ChoiceFacts.v
COQDEP theories/Logic/Berardi.v
COQDEP theories/Init/Wf.v
COQDEP theories/Init/Tactics.v
COQDEP theories/Init/Specif.v
COQDEP theories/Init/Prelude.v
COQDEP theories/Init/Peano.v
COQDEP theories/Init/Notations.v
COQDEP theories/Init/Logic.v
COQDEP theories/Init/Logic_Type.v
COQDEP theories/Init/Datatypes.v
OCAMLLEX ide/config_lexer.mll
30 states, 1657 transitions, table size 6808 bytes
6096 additional bytes used for bindings
OCAMLLEX ide/coq_lex.mll
454 states, 31913 transitions, table size 130376 bytes
OCAMLLEX ide/utf8_convert.mll
15 states, 827 transitions, table size 3398 bytes
OCAMLLEX lib/xml_lexer.mll
78 states, 800 transitions, table size 3668 bytes
OCAMLLEX tools/coqdoc/cpretty.mll
2461 states, 7373 transitions, table size 44258 bytes
OCAMLLEX tools/coqwc.mll
230 states, 833 transitions, table size 4712 bytes
OCAMLLEX tools/gallina_lexer.mll
190 states, 498 transitions, table size 3132 bytes
ECHO... > scripts/tolink.ml
sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' kernel/byterun/coq_instruct.h | \
awk -f kernel/make-opcodes > "kernel/copcodes.ml" || (RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV})
sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
-e '/^}/q' kernel/byterun/coq_instruct.h > "kernel/byterun/coq_jumptbl.h" || (RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV})
ECHO... > plugins/cc/cc_plugin_mod.ml
ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml
ECHO... > plugins/extraction/extraction_plugin_mod.ml
ECHO... > plugins/field/field_plugin_mod.ml
ECHO... > plugins/firstorder/ground_plugin_mod.ml
ECHO... > plugins/fourier/fourier_plugin_mod.ml
ECHO... > plugins/funind/recdef_plugin_mod.ml
ECHO... > plugins/micromega/micromega_plugin_mod.ml
ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
ECHO... > plugins/omega/omega_plugin_mod.ml
ECHO... > plugins/quote/quote_plugin_mod.ml
ECHO... > plugins/ring/ring_plugin_mod.ml
ECHO... > plugins/romega/romega_plugin_mod.ml
ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
ECHO... > plugins/subtac/subtac_plugin_mod.ml
ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
ECHO... > plugins/xml/xml_plugin_mod.ml
COQDEP toplevel/toplevel.mllib
COQDEP tools/win32hack.mllib
COQDEP tactics/tactics.mllib
COQDEP tactics/hightactics.mllib
COQDEP proofs/proofs.mllib
COQDEP pretyping/pretyping.mllib
COQDEP plugins/xml/xml_plugin.mllib
COQDEP plugins/syntax/z_syntax_plugin.mllib
COQDEP plugins/syntax/string_syntax_plugin.mllib
COQDEP plugins/syntax/r_syntax_plugin.mllib
COQDEP plugins/syntax/numbers_syntax_plugin.mllib
COQDEP plugins/syntax/nat_syntax_plugin.mllib
COQDEP plugins/syntax/ascii_syntax_plugin.mllib
COQDEP plugins/subtac/subtac_plugin.mllib
COQDEP plugins/setoid_ring/newring_plugin.mllib
COQDEP plugins/rtauto/rtauto_plugin.mllib
COQDEP plugins/romega/romega_plugin.mllib
COQDEP plugins/ring/ring_plugin.mllib
COQDEP plugins/quote/quote_plugin.mllib
COQDEP plugins/omega/omega_plugin.mllib
COQDEP plugins/nsatz/nsatz_plugin.mllib
COQDEP plugins/micromega/micromega_plugin.mllib
COQDEP plugins/funind/recdef_plugin.mllib
COQDEP plugins/fourier/fourier_plugin.mllib
COQDEP plugins/firstorder/ground_plugin.mllib
COQDEP plugins/field/field_plugin.mllib
COQDEP plugins/extraction/extraction_plugin.mllib
COQDEP plugins/decl_mode/decl_mode_plugin.mllib
COQDEP plugins/cc/cc_plugin.mllib
COQDEP parsing/parsing.mllib
COQDEP parsing/highparsing.mllib
COQDEP parsing/grammar.mllib
COQDEP library/library.mllib
COQDEP lib/lib.mllib
COQDEP kernel/kernel.mllib
COQDEP interp/interp.mllib
COQDEP ide/ide.mllib
COQDEP dev/printers.mllib
COQDEP checker/check.mllib
CCDEP kernel/byterun/coq_values.c
CCDEP kernel/byterun/coq_memory.c
CCDEP kernel/byterun/coq_interp.c
CCDEP kernel/byterun/coq_fix_code.c
CCDEP ide/ide_win32_stubs.c
CCDEP ide/ide_mac_stubs.c
OCAMLDEP toplevel/whelp.mli
OCAMLDEP toplevel/vernacinterp.mli
OCAMLDEP toplevel/vernacentries.mli
OCAMLDEP toplevel/vernac.mli
OCAMLDEP toplevel/usage.mli
OCAMLDEP toplevel/toplevel.mli
OCAMLDEP toplevel/search.mli
OCAMLDEP toplevel/record.mli
OCAMLDEP toplevel/mltop.mli
OCAMLDEP toplevel/metasyntax.mli
OCAMLDEP toplevel/libtypes.mli
OCAMLDEP toplevel/lemmas.mli
OCAMLDEP toplevel/interface.mli
OCAMLDEP toplevel/indschemes.mli
OCAMLDEP toplevel/ind_tables.mli
OCAMLDEP toplevel/ide_slave.mli
OCAMLDEP toplevel/ide_intf.mli
OCAMLDEP toplevel/himsg.mli
OCAMLDEP toplevel/discharge.mli
OCAMLDEP toplevel/coqtop.mli
OCAMLDEP toplevel/coqinit.mli
OCAMLDEP toplevel/command.mli
OCAMLDEP toplevel/classes.mli
OCAMLDEP toplevel/class.mli
OCAMLDEP toplevel/cerrors.mli
OCAMLDEP toplevel/backtrack.mli
OCAMLDEP toplevel/autoinstance.mli
OCAMLDEP toplevel/auto_ind_decl.mli
OCAMLDEP tools/coqdoc/tokens.mli
OCAMLDEP tools/coqdoc/output.mli
OCAMLDEP tools/coqdoc/index.mli
OCAMLDEP tools/coqdoc/cpretty.mli
OCAMLDEP tools/coqdoc/alpha.mli
OCAMLDEP tools/coqdep_lexer.mli
OCAMLDEP tools/coqdep_common.mli
OCAMLDEP tactics/termdn.mli
OCAMLDEP tactics/tactics.mli
OCAMLDEP tactics/tacticals.mli
OCAMLDEP tactics/tactic_option.mli
OCAMLDEP tactics/tacinterp.mli
OCAMLDEP tactics/refine.mli
OCAMLDEP tactics/nbtermdn.mli
OCAMLDEP tactics/leminv.mli
OCAMLDEP tactics/inv.mli
OCAMLDEP tactics/hipattern.mli
OCAMLDEP tactics/hiddentac.mli
OCAMLDEP tactics/extratactics.mli
OCAMLDEP tactics/extraargs.mli
OCAMLDEP tactics/evar_tactics.mli
OCAMLDEP tactics/equality.mli
OCAMLDEP tactics/eqschemes.mli
OCAMLDEP tactics/elimschemes.mli
OCAMLDEP tactics/elim.mli
OCAMLDEP tactics/eauto.mli
OCAMLDEP tactics/dn.mli
OCAMLDEP tactics/contradiction.mli
OCAMLDEP tactics/btermdn.mli
OCAMLDEP tactics/autorewrite.mli
OCAMLDEP tactics/auto.mli
OCAMLDEP proofs/tactic_debug.mli
OCAMLDEP proofs/tacmach.mli
OCAMLDEP proofs/refiner.mli
OCAMLDEP proofs/redexpr.mli
OCAMLDEP proofs/proofview.mli
OCAMLDEP proofs/proof_type.mli
OCAMLDEP proofs/proof_global.mli
OCAMLDEP proofs/proof.mli
OCAMLDEP proofs/pfedit.mli
OCAMLDEP proofs/logic.mli
OCAMLDEP proofs/goal.mli
OCAMLDEP proofs/evar_refiner.mli
OCAMLDEP proofs/clenvtac.mli
OCAMLDEP proofs/clenv.mli
OCAMLDEP pretyping/vnorm.mli
OCAMLDEP pretyping/unification.mli
OCAMLDEP pretyping/typing.mli
OCAMLDEP pretyping/typeclasses_errors.mli
OCAMLDEP pretyping/typeclasses.mli
OCAMLDEP pretyping/termops.mli
OCAMLDEP pretyping/term_dnet.mli
OCAMLDEP pretyping/tacred.mli
OCAMLDEP pretyping/retyping.mli
OCAMLDEP pretyping/reductionops.mli
OCAMLDEP pretyping/recordops.mli
OCAMLDEP pretyping/pretyping.mli
OCAMLDEP pretyping/pretype_errors.mli
OCAMLDEP pretyping/pattern.mli
OCAMLDEP pretyping/namegen.mli
OCAMLDEP pretyping/matching.mli
OCAMLDEP pretyping/inductiveops.mli
OCAMLDEP pretyping/indrec.mli
OCAMLDEP pretyping/glob_term.mli
OCAMLDEP pretyping/evd.mli
OCAMLDEP pretyping/evarutil.mli
OCAMLDEP pretyping/evarconv.mli
OCAMLDEP pretyping/detyping.mli
OCAMLDEP pretyping/coercion.mli
OCAMLDEP pretyping/classops.mli
OCAMLDEP pretyping/cbv.mli
OCAMLDEP pretyping/cases.mli
OCAMLDEP pretyping/arguments_renaming.mli
OCAMLDEP plugins/xml/xmlcommand.mli
OCAMLDEP plugins/xml/xml.mli
OCAMLDEP plugins/xml/unshare.mli
OCAMLDEP plugins/xml/doubleTypeInference.mli
OCAMLDEP plugins/subtac/subtac_utils.mli
OCAMLDEP plugins/subtac/subtac_pretyping.mli
OCAMLDEP plugins/subtac/subtac_obligations.mli
OCAMLDEP plugins/subtac/subtac_errors.mli
OCAMLDEP plugins/subtac/subtac_command.mli
OCAMLDEP plugins/subtac/subtac_coercion.mli
OCAMLDEP plugins/subtac/subtac_classes.mli
OCAMLDEP plugins/subtac/subtac_cases.mli
OCAMLDEP plugins/subtac/subtac.mli
OCAMLDEP plugins/subtac/eterm.mli
OCAMLDEP plugins/rtauto/refl_tauto.mli
OCAMLDEP plugins/rtauto/proof_search.mli
OCAMLDEP plugins/romega/const_omega.mli
OCAMLDEP plugins/nsatz/utile.mli
OCAMLDEP plugins/nsatz/polynom.mli
OCAMLDEP plugins/micromega/sos.mli
OCAMLDEP plugins/micromega/micromega.mli
OCAMLDEP plugins/funind/indfun_common.mli
OCAMLDEP plugins/funind/indfun.mli
OCAMLDEP plugins/funind/glob_termops.mli
OCAMLDEP plugins/funind/glob_term_to_relation.mli
OCAMLDEP plugins/funind/functional_principles_types.mli
OCAMLDEP plugins/funind/functional_principles_proofs.mli
OCAMLDEP plugins/firstorder/unify.mli
OCAMLDEP plugins/firstorder/sequent.mli
OCAMLDEP plugins/firstorder/rules.mli
OCAMLDEP plugins/firstorder/instances.mli
OCAMLDEP plugins/firstorder/ground.mli
OCAMLDEP plugins/firstorder/formula.mli
OCAMLDEP plugins/extraction/table.mli
OCAMLDEP plugins/extraction/scheme.mli
OCAMLDEP plugins/extraction/ocaml.mli
OCAMLDEP plugins/extraction/modutil.mli
OCAMLDEP plugins/extraction/mlutil.mli
OCAMLDEP plugins/extraction/miniml.mli
OCAMLDEP plugins/extraction/haskell.mli
OCAMLDEP plugins/extraction/extraction.mli
OCAMLDEP plugins/extraction/extract_env.mli
OCAMLDEP plugins/extraction/common.mli
OCAMLDEP plugins/decl_mode/ppdecl_proof.mli
OCAMLDEP plugins/decl_mode/decl_proof_instr.mli
OCAMLDEP plugins/decl_mode/decl_mode.mli
OCAMLDEP plugins/decl_mode/decl_interp.mli
OCAMLDEP plugins/decl_mode/decl_expr.mli
OCAMLDEP plugins/cc/cctac.mli
OCAMLDEP plugins/cc/ccproof.mli
OCAMLDEP plugins/cc/ccalgo.mli
OCAMLDEP parsing/tok.mli
OCAMLDEP parsing/tactic_printer.mli
OCAMLDEP parsing/q_util.mli
OCAMLDEP parsing/printmod.mli
OCAMLDEP parsing/printer.mli
OCAMLDEP parsing/prettyp.mli
OCAMLDEP parsing/ppvernac.mli
OCAMLDEP parsing/pptactic.mli
OCAMLDEP parsing/ppconstr.mli
OCAMLDEP parsing/pcoq.mli
OCAMLDEP parsing/lexer.mli
OCAMLDEP parsing/extrawit.mli
OCAMLDEP parsing/extend.mli
OCAMLDEP parsing/egrammar.mli
OCAMLDEP library/summary.mli
OCAMLDEP library/states.mli
OCAMLDEP library/nametab.mli
OCAMLDEP library/nameops.mli
OCAMLDEP library/library.mli
OCAMLDEP library/libobject.mli
OCAMLDEP library/libnames.mli
OCAMLDEP library/lib.mli
OCAMLDEP library/impargs.mli
OCAMLDEP library/heads.mli
OCAMLDEP library/goptionstyp.mli
OCAMLDEP library/goptions.mli
OCAMLDEP library/global.mli
OCAMLDEP library/dischargedhypsmap.mli
OCAMLDEP library/decls.mli
OCAMLDEP library/declaremods.mli
OCAMLDEP library/declare.mli
OCAMLDEP library/decl_kinds.mli
OCAMLDEP library/assumptions.mli
OCAMLDEP lib/xml_utils.mli
OCAMLDEP lib/xml_parser.mli
OCAMLDEP lib/xml_lexer.mli
OCAMLDEP lib/util.mli
OCAMLDEP lib/unionfind.mli
OCAMLDEP lib/tries.mli
OCAMLDEP lib/system.mli
OCAMLDEP lib/store.mli
OCAMLDEP lib/segmenttree.mli
OCAMLDEP lib/rtree.mli
OCAMLDEP lib/profile.mli
OCAMLDEP lib/predicate.mli
OCAMLDEP lib/pp_control.mli
OCAMLDEP lib/pp.mli
OCAMLDEP lib/option.mli
OCAMLDEP lib/heap.mli
OCAMLDEP lib/hashtbl_alt.mli
OCAMLDEP lib/hashcons.mli
OCAMLDEP lib/gmapl.mli
OCAMLDEP lib/gmap.mli
OCAMLDEP lib/fset.mli
OCAMLDEP lib/fmap.mli
OCAMLDEP lib/flags.mli
OCAMLDEP lib/explore.mli
OCAMLDEP lib/errors.mli
OCAMLDEP lib/envars.mli
OCAMLDEP lib/dyn.mli
OCAMLDEP lib/dnet.mli
OCAMLDEP lib/bigint.mli
OCAMLDEP kernel/vm.mli
OCAMLDEP kernel/vconv.mli
OCAMLDEP kernel/univ.mli
OCAMLDEP kernel/typeops.mli
OCAMLDEP kernel/type_errors.mli
OCAMLDEP kernel/term_typing.mli
OCAMLDEP kernel/term.mli
OCAMLDEP kernel/subtyping.mli
OCAMLDEP kernel/sign.mli
OCAMLDEP kernel/safe_typing.mli
OCAMLDEP kernel/retroknowledge.mli
OCAMLDEP kernel/reduction.mli
OCAMLDEP kernel/pre_env.mli
OCAMLDEP kernel/names.mli
OCAMLDEP kernel/modops.mli
OCAMLDEP kernel/mod_typing.mli
OCAMLDEP kernel/mod_subst.mli
OCAMLDEP kernel/inductive.mli
OCAMLDEP kernel/indtypes.mli
OCAMLDEP kernel/esubst.mli
OCAMLDEP kernel/environ.mli
OCAMLDEP kernel/entries.mli
OCAMLDEP kernel/declarations.mli
OCAMLDEP kernel/csymtable.mli
OCAMLDEP kernel/cooking.mli
OCAMLDEP kernel/conv_oracle.mli
OCAMLDEP kernel/closure.mli
OCAMLDEP kernel/cemitcodes.mli
OCAMLDEP kernel/cbytegen.mli
OCAMLDEP kernel/cbytecodes.mli
OCAMLDEP interp/topconstr.mli
OCAMLDEP interp/syntax_def.mli
OCAMLDEP interp/smartlocate.mli
OCAMLDEP interp/reserve.mli
OCAMLDEP interp/ppextend.mli
OCAMLDEP interp/notation.mli
OCAMLDEP interp/modintern.mli
OCAMLDEP interp/implicit_quantifiers.mli
OCAMLDEP interp/genarg.mli
OCAMLDEP interp/dumpglob.mli
OCAMLDEP interp/coqlib.mli
OCAMLDEP interp/constrintern.mli
OCAMLDEP interp/constrextern.mli
OCAMLDEP ide/utils/okey.mli
OCAMLDEP ide/utils/configwin.mli
OCAMLDEP ide/utils/config_file.mli
OCAMLDEP ide/undo_lablgtk_lt26.mli
OCAMLDEP ide/undo_lablgtk_ge26.mli
OCAMLDEP ide/undo_lablgtk_ge212.mli
OCAMLDEP ide/tags.mli
OCAMLDEP ide/preferences.mli
OCAMLDEP ide/minilib.mli
OCAMLDEP ide/ideutils.mli
OCAMLDEP ide/coqide.mli
OCAMLDEP ide/coq.mli
OCAMLDEP ide/command_windows.mli
OCAMLDEP config/coq_config.mli
OCAMLDEP checker/typeops.mli
OCAMLDEP checker/type_errors.mli
OCAMLDEP checker/term.mli
OCAMLDEP checker/subtyping.mli
OCAMLDEP checker/safe_typing.mli
OCAMLDEP checker/reduction.mli
OCAMLDEP checker/modops.mli
OCAMLDEP checker/mod_checking.mli
OCAMLDEP checker/inductive.mli
OCAMLDEP checker/indtypes.mli
OCAMLDEP checker/environ.mli
OCAMLDEP checker/declarations.mli
OCAMLDEP checker/closure.mli
OCAMLDEP checker/check_stat.mli
OCAMLDEP plugins/xml/xml_plugin_mod.ml
OCAMLDEP plugins/syntax/z_syntax_plugin_mod.ml
OCAMLDEP plugins/syntax/string_syntax_plugin_mod.ml
OCAMLDEP plugins/syntax/r_syntax_plugin_mod.ml
OCAMLDEP plugins/syntax/numbers_syntax_plugin_mod.ml
OCAMLDEP plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLDEP plugins/syntax/ascii_syntax_plugin_mod.ml
OCAMLDEP plugins/subtac/subtac_plugin_mod.ml
OCAMLDEP plugins/setoid_ring/newring_plugin_mod.ml
OCAMLDEP plugins/rtauto/rtauto_plugin_mod.ml
OCAMLDEP plugins/romega/romega_plugin_mod.ml
OCAMLDEP plugins/ring/ring_plugin_mod.ml
OCAMLDEP plugins/quote/quote_plugin_mod.ml
OCAMLDEP plugins/omega/omega_plugin_mod.ml
OCAMLDEP plugins/nsatz/nsatz_plugin_mod.ml
OCAMLDEP plugins/micromega/micromega_plugin_mod.ml
OCAMLDEP plugins/funind/recdef_plugin_mod.ml
OCAMLDEP plugins/fourier/fourier_plugin_mod.ml
OCAMLDEP plugins/firstorder/ground_plugin_mod.ml
OCAMLDEP plugins/field/field_plugin_mod.ml
OCAMLDEP plugins/extraction/extraction_plugin_mod.ml
OCAMLDEP plugins/decl_mode/decl_mode_plugin_mod.ml
OCAMLDEP plugins/cc/cc_plugin_mod.ml
"ocamlc" -rectypes -c tools/compat5.ml
"ocamlc" -rectypes -c tools/compat5b.ml
CAMLP4DEPS toplevel/whelp.ml4
CAMLP4O toplevel/whelp.ml4
toplevel/whelp.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4O toplevel/mltop.ml4
OCAMLDEP toplevel/mltop.ml
CAMLP4DEPS tools/coq_tex.ml4
CAMLP4O tools/coq_tex.ml4
OCAMLDEP tools/coq_tex.ml
CAMLP4DEPS tactics/tauto.ml4
CAMLP4O tactics/tauto.ml4
tactics/tauto.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/rewrite.ml4
CAMLP4O tactics/rewrite.ml4
tactics/rewrite.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/hipattern.ml4
CAMLP4O tactics/hipattern.ml4
tactics/hipattern.ml4 : Dependency parsing/grammar.cma parsing/q_constr.cmo not ready yet
CAMLP4DEPS tactics/extratactics.ml4
CAMLP4O tactics/extratactics.ml4
tactics/extratactics.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/extraargs.ml4
CAMLP4O tactics/extraargs.ml4
tactics/extraargs.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/eqdecide.ml4
CAMLP4O tactics/eqdecide.ml4
tactics/eqdecide.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/eauto.ml4
CAMLP4O tactics/eauto.ml4
tactics/eauto.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS tactics/class_tactics.ml4
CAMLP4O tactics/class_tactics.ml4
tactics/class_tactics.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/xml/xmlentries.ml4
CAMLP4O plugins/xml/xmlentries.ml4
plugins/xml/xmlentries.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/xml/xml.ml4
CAMLP4O plugins/xml/xml.ml4
OCAMLDEP plugins/xml/xml.ml
CAMLP4DEPS plugins/xml/proofTree2Xml.ml4
CAMLP4O plugins/xml/proofTree2Xml.ml4
OCAMLDEP plugins/xml/proofTree2Xml.ml
CAMLP4DEPS plugins/xml/dumptree.ml4
CAMLP4O plugins/xml/dumptree.ml4
plugins/xml/dumptree.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/xml/acic2Xml.ml4
CAMLP4O plugins/xml/acic2Xml.ml4
OCAMLDEP plugins/xml/acic2Xml.ml
CAMLP4DEPS plugins/subtac/g_subtac.ml4
CAMLP4O plugins/subtac/g_subtac.ml4
plugins/subtac/g_subtac.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/setoid_ring/newring.ml4
CAMLP4O plugins/setoid_ring/newring.ml4
plugins/setoid_ring/newring.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/rtauto/g_rtauto.ml4
CAMLP4O plugins/rtauto/g_rtauto.ml4
plugins/rtauto/g_rtauto.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/romega/g_romega.ml4
CAMLP4O plugins/romega/g_romega.ml4
plugins/romega/g_romega.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/ring/g_ring.ml4
CAMLP4O plugins/ring/g_ring.ml4
plugins/ring/g_ring.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/quote/g_quote.ml4
CAMLP4O plugins/quote/g_quote.ml4
plugins/quote/g_quote.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/omega/g_omega.ml4
CAMLP4O plugins/omega/g_omega.ml4
plugins/omega/g_omega.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/nsatz/nsatz.ml4
CAMLP4O plugins/nsatz/nsatz.ml4
plugins/nsatz/nsatz.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/micromega/g_micromega.ml4
CAMLP4O plugins/micromega/g_micromega.ml4
plugins/micromega/g_micromega.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/funind/g_indfun.ml4
CAMLP4O plugins/funind/g_indfun.ml4
plugins/funind/g_indfun.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/fourier/g_fourier.ml4
CAMLP4O plugins/fourier/g_fourier.ml4
plugins/fourier/g_fourier.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/firstorder/g_ground.ml4
CAMLP4O plugins/firstorder/g_ground.ml4
plugins/firstorder/g_ground.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/field/field.ml4
CAMLP4O plugins/field/field.ml4
plugins/field/field.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/extraction/g_extraction.ml4
CAMLP4O plugins/extraction/g_extraction.ml4
plugins/extraction/g_extraction.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/decl_mode/g_decl_mode.ml4
CAMLP4O plugins/decl_mode/g_decl_mode.ml4
plugins/decl_mode/g_decl_mode.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS plugins/cc/g_congruence.ml4
CAMLP4O plugins/cc/g_congruence.ml4
plugins/cc/g_congruence.ml4 : Dependency parsing/grammar.cma not ready yet
CAMLP4DEPS parsing/vernacextend.ml4
CAMLP4O parsing/vernacextend.ml4
OCAMLDEP parsing/vernacextend.ml
CAMLP4DEPS parsing/tacextend.ml4
CAMLP4O parsing/tacextend.ml4
OCAMLDEP parsing/tacextend.ml
CAMLP4DEPS parsing/q_util.ml4
CAMLP4O parsing/q_util.ml4
OCAMLDEP parsing/q_util.ml
CAMLP4DEPS parsing/q_coqast.ml4
CAMLP4O parsing/q_coqast.ml4
OCAMLDEP parsing/q_coqast.ml
CAMLP4DEPS parsing/q_constr.ml4
CAMLP4O parsing/q_constr.ml4
OCAMLDEP parsing/q_constr.ml
CAMLP4DEPS parsing/pcoq.ml4
CAMLP4O parsing/pcoq.ml4
OCAMLDEP parsing/pcoq.ml
CAMLP4DEPS parsing/lexer.ml4
CAMLP4O parsing/lexer.ml4
OCAMLDEP parsing/lexer.ml
CAMLP4DEPS parsing/g_xml.ml4
CAMLP4O parsing/g_xml.ml4
OCAMLDEP parsing/g_xml.ml
CAMLP4DEPS parsing/g_vernac.ml4
CAMLP4O parsing/g_vernac.ml4
OCAMLDEP parsing/g_vernac.ml
CAMLP4DEPS parsing/g_tactic.ml4
CAMLP4O parsing/g_tactic.ml4
OCAMLDEP parsing/g_tactic.ml
CAMLP4DEPS parsing/g_proofs.ml4
CAMLP4O parsing/g_proofs.ml4
OCAMLDEP parsing/g_proofs.ml
CAMLP4DEPS parsing/g_prim.ml4
CAMLP4O parsing/g_prim.ml4
OCAMLDEP parsing/g_prim.ml
CAMLP4DEPS parsing/g_ltac.ml4
CAMLP4O parsing/g_ltac.ml4
OCAMLDEP parsing/g_ltac.ml
CAMLP4DEPS parsing/g_constr.ml4
CAMLP4O parsing/g_constr.ml4
OCAMLDEP parsing/g_constr.ml
CAMLP4DEPS parsing/argextend.ml4
CAMLP4O parsing/argextend.ml4
OCAMLDEP parsing/argextend.ml
CAMLP4DEPS lib/pp.ml4
CAMLP4O lib/pp.ml4
OCAMLDEP lib/pp.ml
CAMLP4DEPS lib/compat.ml4
CAMLP4O lib/compat.ml4
OCAMLDEP lib/compat.ml
CAMLP4DEPS ide/project_file.ml4
CAMLP4O ide/project_file.ml4
OCAMLDEP ide/project_file.ml
CAMLP4O ide/coqide_main.ml4
OCAMLDEP ide/coqide_main.ml
OCAMLDEP kernel/copcodes.ml
OCAMLDEP scripts/tolink.ml
OCAMLDEP tools/gallina_lexer.ml
OCAMLDEP tools/coqwc.ml
OCAMLDEP tools/coqdoc/cpretty.ml
OCAMLDEP tools/coqdep_lexer.ml
OCAMLDEP lib/xml_lexer.ml
OCAMLDEP ide/utf8_convert.ml
OCAMLDEP ide/coq_lex.ml
OCAMLDEP ide/config_lexer.ml
OCAMLDEP toplevel/vernacinterp.ml
OCAMLDEP toplevel/vernacexpr.ml
OCAMLDEP toplevel/vernacentries.ml
OCAMLDEP toplevel/vernac.ml
OCAMLDEP toplevel/usage.ml
OCAMLDEP toplevel/toplevel.ml
OCAMLDEP toplevel/search.ml
OCAMLDEP toplevel/record.ml
OCAMLDEP toplevel/metasyntax.ml
OCAMLDEP toplevel/libtypes.ml
OCAMLDEP toplevel/lemmas.ml
OCAMLDEP toplevel/indschemes.ml
OCAMLDEP toplevel/ind_tables.ml
OCAMLDEP toplevel/ide_slave.ml
OCAMLDEP toplevel/ide_intf.ml
OCAMLDEP toplevel/himsg.ml
OCAMLDEP toplevel/discharge.ml
OCAMLDEP toplevel/coqtop.ml
OCAMLDEP toplevel/coqinit.ml
OCAMLDEP toplevel/command.ml
OCAMLDEP toplevel/classes.ml
OCAMLDEP toplevel/class.ml
OCAMLDEP toplevel/cerrors.ml
OCAMLDEP toplevel/backtrack.ml
OCAMLDEP toplevel/autoinstance.ml
OCAMLDEP toplevel/auto_ind_decl.ml
OCAMLDEP tools/win32hack_filename.ml
OCAMLDEP tools/mkwinapp.ml
OCAMLDEP tools/mingwpath.ml
OCAMLDEP tools/gallina.ml
OCAMLDEP tools/fake_ide.ml
OCAMLDEP tools/escape_string.ml
OCAMLDEP tools/coqdoc/tokens.ml
OCAMLDEP tools/coqdoc/output.ml
OCAMLDEP tools/coqdoc/main.ml
OCAMLDEP tools/coqdoc/index.ml
OCAMLDEP tools/coqdoc/cdglobals.ml
OCAMLDEP tools/coqdoc/alpha.ml
OCAMLDEP tools/coqdep_common.ml
OCAMLDEP tools/coqdep_boot.ml
OCAMLDEP tools/coqdep.ml
OCAMLDEP tools/coq_makefile.ml
OCAMLDEP tools/compat5b.ml
OCAMLDEP tools/compat5.ml
OCAMLDEP theories/Numbers/Natural/BigN/NMake_gen.ml
OCAMLDEP tactics/termdn.ml
OCAMLDEP tactics/tactics.ml
OCAMLDEP tactics/tacticals.ml
OCAMLDEP tactics/tactic_option.ml
OCAMLDEP tactics/tacinterp.ml
OCAMLDEP tactics/refine.ml
OCAMLDEP tactics/nbtermdn.ml
OCAMLDEP tactics/leminv.ml
OCAMLDEP tactics/inv.ml
OCAMLDEP tactics/hiddentac.ml
OCAMLDEP tactics/evar_tactics.ml
OCAMLDEP tactics/equality.ml
OCAMLDEP tactics/eqschemes.ml
OCAMLDEP tactics/elimschemes.ml
OCAMLDEP tactics/elim.ml
OCAMLDEP tactics/dn.ml
OCAMLDEP tactics/contradiction.ml
OCAMLDEP tactics/btermdn.ml
OCAMLDEP tactics/autorewrite.ml
OCAMLDEP tactics/auto.ml
OCAMLDEP scripts/coqmktop.ml
OCAMLDEP scripts/coqc.ml
OCAMLDEP proofs/tactic_debug.ml
OCAMLDEP proofs/tacmach.ml
OCAMLDEP proofs/tacexpr.ml
OCAMLDEP proofs/refiner.ml
OCAMLDEP proofs/redexpr.ml
OCAMLDEP proofs/proofview.ml
OCAMLDEP proofs/proof_type.ml
OCAMLDEP proofs/proof_global.ml
OCAMLDEP proofs/proof.ml
OCAMLDEP proofs/pfedit.ml
OCAMLDEP proofs/logic.ml
OCAMLDEP proofs/goal.ml
OCAMLDEP proofs/evar_refiner.ml
OCAMLDEP proofs/clenvtac.ml
OCAMLDEP proofs/clenv.ml
OCAMLDEP pretyping/vnorm.ml
OCAMLDEP pretyping/unification.ml
OCAMLDEP pretyping/typing.ml
OCAMLDEP pretyping/typeclasses_errors.ml
OCAMLDEP pretyping/typeclasses.ml
OCAMLDEP pretyping/termops.ml
OCAMLDEP pretyping/term_dnet.ml
OCAMLDEP pretyping/tacred.ml
OCAMLDEP pretyping/retyping.ml
OCAMLDEP pretyping/reductionops.ml
OCAMLDEP pretyping/recordops.ml
OCAMLDEP pretyping/pretyping.ml
OCAMLDEP pretyping/pretype_errors.ml
OCAMLDEP pretyping/pattern.ml
OCAMLDEP pretyping/namegen.ml
OCAMLDEP pretyping/matching.ml
OCAMLDEP pretyping/inductiveops.ml
OCAMLDEP pretyping/indrec.ml
OCAMLDEP pretyping/glob_term.ml
OCAMLDEP pretyping/evd.ml
OCAMLDEP pretyping/evarutil.ml
OCAMLDEP pretyping/evarconv.ml
OCAMLDEP pretyping/detyping.ml
OCAMLDEP pretyping/coercion.ml
OCAMLDEP pretyping/classops.ml
OCAMLDEP pretyping/cbv.ml
OCAMLDEP pretyping/cases.ml
OCAMLDEP pretyping/arguments_renaming.ml
OCAMLDEP plugins/xml/xmlcommand.ml
OCAMLDEP plugins/xml/unshare.ml
OCAMLDEP plugins/xml/proof2aproof.ml
OCAMLDEP plugins/xml/doubleTypeInference.ml
OCAMLDEP plugins/xml/cic2Xml.ml
OCAMLDEP plugins/xml/cic2acic.ml
OCAMLDEP plugins/xml/acic.ml
OCAMLDEP plugins/syntax/z_syntax.ml
OCAMLDEP plugins/syntax/string_syntax.ml
OCAMLDEP plugins/syntax/r_syntax.ml
OCAMLDEP plugins/syntax/numbers_syntax.ml
OCAMLDEP plugins/syntax/nat_syntax.ml
OCAMLDEP plugins/syntax/ascii_syntax.ml
OCAMLDEP plugins/subtac/subtac_utils.ml
OCAMLDEP plugins/subtac/subtac_pretyping_F.ml
OCAMLDEP plugins/subtac/subtac_pretyping.ml
OCAMLDEP plugins/subtac/subtac_obligations.ml
OCAMLDEP plugins/subtac/subtac_errors.ml
OCAMLDEP plugins/subtac/subtac_command.ml
OCAMLDEP plugins/subtac/subtac_coercion.ml
OCAMLDEP plugins/subtac/subtac_classes.ml
OCAMLDEP plugins/subtac/subtac_cases.ml
OCAMLDEP plugins/subtac/subtac.ml
OCAMLDEP plugins/subtac/eterm.ml
OCAMLDEP plugins/rtauto/refl_tauto.ml
OCAMLDEP plugins/rtauto/proof_search.ml
OCAMLDEP plugins/romega/refl_omega.ml
OCAMLDEP plugins/romega/const_omega.ml
OCAMLDEP plugins/ring/ring.ml
OCAMLDEP plugins/quote/quote.ml
OCAMLDEP plugins/omega/omega.ml
OCAMLDEP plugins/omega/coq_omega.ml
OCAMLDEP plugins/nsatz/utile.ml
OCAMLDEP plugins/nsatz/polynom.ml
OCAMLDEP plugins/nsatz/ideal.ml
OCAMLDEP plugins/micromega/sos_types.ml
OCAMLDEP plugins/micromega/sos_lib.ml
OCAMLDEP plugins/micromega/sos.ml
OCAMLDEP plugins/micromega/polynomial.ml
OCAMLDEP plugins/micromega/persistent_cache.ml
OCAMLDEP plugins/micromega/mutils.ml
OCAMLDEP plugins/micromega/micromega.ml
OCAMLDEP plugins/micromega/mfourier.ml
OCAMLDEP plugins/micromega/csdpcert.ml
OCAMLDEP plugins/micromega/coq_micromega.ml
OCAMLDEP plugins/micromega/certificate.ml
OCAMLDEP plugins/funind/recdef.ml
OCAMLDEP plugins/funind/merge.ml
OCAMLDEP plugins/funind/invfun.ml
OCAMLDEP plugins/funind/indfun_common.ml
OCAMLDEP plugins/funind/indfun.ml
OCAMLDEP plugins/funind/glob_termops.ml
OCAMLDEP plugins/funind/glob_term_to_relation.ml
OCAMLDEP plugins/funind/functional_principles_types.ml
OCAMLDEP plugins/funind/functional_principles_proofs.ml
OCAMLDEP plugins/fourier/fourierR.ml
OCAMLDEP plugins/fourier/fourier.ml
OCAMLDEP plugins/firstorder/unify.ml
OCAMLDEP plugins/firstorder/sequent.ml
OCAMLDEP plugins/firstorder/rules.ml
OCAMLDEP plugins/firstorder/instances.ml
OCAMLDEP plugins/firstorder/ground.ml
OCAMLDEP plugins/firstorder/formula.ml
OCAMLDEP plugins/extraction/table.ml
OCAMLDEP plugins/extraction/scheme.ml
OCAMLDEP plugins/extraction/ocaml.ml
OCAMLDEP plugins/extraction/modutil.ml
OCAMLDEP plugins/extraction/mlutil.ml
OCAMLDEP plugins/extraction/haskell.ml
OCAMLDEP plugins/extraction/extraction.ml
OCAMLDEP plugins/extraction/extract_env.ml
OCAMLDEP plugins/extraction/common.ml
OCAMLDEP plugins/extraction/big.ml
OCAMLDEP plugins/decl_mode/ppdecl_proof.ml
OCAMLDEP plugins/decl_mode/decl_proof_instr.ml
OCAMLDEP plugins/decl_mode/decl_mode.ml
OCAMLDEP plugins/decl_mode/decl_interp.ml
OCAMLDEP plugins/cc/cctac.ml
OCAMLDEP plugins/cc/ccproof.ml
OCAMLDEP plugins/cc/ccalgo.ml
OCAMLDEP parsing/tok.ml
OCAMLDEP parsing/tactic_printer.ml
OCAMLDEP parsing/printmod.ml
OCAMLDEP parsing/printer.ml
OCAMLDEP parsing/prettyp.ml
OCAMLDEP parsing/ppvernac.ml
OCAMLDEP parsing/pptactic.ml
OCAMLDEP parsing/ppconstr.ml
OCAMLDEP parsing/extrawit.ml
OCAMLDEP parsing/extend.ml
OCAMLDEP parsing/egrammar.ml
OCAMLDEP myocamlbuild.ml
OCAMLDEP library/summary.ml
OCAMLDEP library/states.ml
OCAMLDEP library/nametab.ml
OCAMLDEP library/nameops.ml
OCAMLDEP library/library.ml
OCAMLDEP library/libobject.ml
OCAMLDEP library/libnames.ml
OCAMLDEP library/lib.ml
OCAMLDEP library/impargs.ml
OCAMLDEP library/heads.ml
OCAMLDEP library/goptions.ml
OCAMLDEP library/global.ml
OCAMLDEP library/dischargedhypsmap.ml
OCAMLDEP library/decls.ml
OCAMLDEP library/declaremods.ml
OCAMLDEP library/declare.ml
OCAMLDEP library/decl_kinds.ml
OCAMLDEP library/assumptions.ml
OCAMLDEP lib/xml_utils.ml
OCAMLDEP lib/xml_parser.ml
OCAMLDEP lib/util.ml
OCAMLDEP lib/unionfind.ml
OCAMLDEP lib/unicodetable.ml
OCAMLDEP lib/tries.ml
OCAMLDEP lib/system.ml
OCAMLDEP lib/store.ml
OCAMLDEP lib/segmenttree.ml
OCAMLDEP lib/rtree.ml
OCAMLDEP lib/profile.ml
OCAMLDEP lib/predicate.ml
OCAMLDEP lib/pp_control.ml
OCAMLDEP lib/option.ml
OCAMLDEP lib/heap.ml
OCAMLDEP lib/hashtbl_alt.ml
OCAMLDEP lib/hashcons.ml
OCAMLDEP lib/gmapl.ml
OCAMLDEP lib/gmap.ml
OCAMLDEP lib/fset.ml
OCAMLDEP lib/fmap.ml
OCAMLDEP lib/flags.ml
OCAMLDEP lib/explore.ml
OCAMLDEP lib/errors.ml
OCAMLDEP lib/envars.ml
OCAMLDEP lib/dyn.ml
OCAMLDEP lib/dnet.ml
OCAMLDEP lib/bigint.ml
OCAMLDEP kernel/vm.ml
OCAMLDEP kernel/vconv.ml
OCAMLDEP kernel/univ.ml
OCAMLDEP kernel/typeops.ml
OCAMLDEP kernel/type_errors.ml
OCAMLDEP kernel/term_typing.ml
OCAMLDEP kernel/term.ml
OCAMLDEP kernel/subtyping.ml
OCAMLDEP kernel/sign.ml
OCAMLDEP kernel/safe_typing.ml
OCAMLDEP kernel/retroknowledge.ml
OCAMLDEP kernel/reduction.ml
OCAMLDEP kernel/pre_env.ml
OCAMLDEP kernel/names.ml
OCAMLDEP kernel/modops.ml
OCAMLDEP kernel/mod_typing.ml
OCAMLDEP kernel/mod_subst.ml
OCAMLDEP kernel/inductive.ml
OCAMLDEP kernel/indtypes.ml
OCAMLDEP kernel/esubst.ml
OCAMLDEP kernel/environ.ml
OCAMLDEP kernel/entries.ml
OCAMLDEP kernel/declarations.ml
OCAMLDEP kernel/csymtable.ml
OCAMLDEP kernel/cooking.ml
OCAMLDEP kernel/conv_oracle.ml
OCAMLDEP kernel/closure.ml
OCAMLDEP kernel/cemitcodes.ml
OCAMLDEP kernel/cbytegen.ml
OCAMLDEP kernel/cbytecodes.ml
OCAMLDEP interp/topconstr.ml
OCAMLDEP interp/syntax_def.ml
OCAMLDEP interp/smartlocate.ml
OCAMLDEP interp/reserve.ml
OCAMLDEP interp/ppextend.ml
OCAMLDEP interp/notation.ml
OCAMLDEP interp/modintern.ml
OCAMLDEP interp/implicit_quantifiers.ml
OCAMLDEP interp/genarg.ml
OCAMLDEP interp/dumpglob.ml
OCAMLDEP interp/coqlib.ml
OCAMLDEP interp/constrintern.ml
OCAMLDEP interp/constrextern.ml
OCAMLDEP ide/utils/okey.ml
OCAMLDEP ide/utils/editable_cells.ml
OCAMLDEP ide/utils/configwin_types.ml
OCAMLDEP ide/utils/configwin_messages.ml
OCAMLDEP ide/utils/configwin_keys.ml
OCAMLDEP ide/utils/configwin_ihm.ml
OCAMLDEP ide/utils/configwin.ml
OCAMLDEP ide/utils/config_file.ml
OCAMLDEP ide/undo.ml
OCAMLDEP ide/typed_notebook.ml
OCAMLDEP ide/tags.ml
OCAMLDEP ide/preferences.ml
OCAMLDEP ide/minilib.ml
OCAMLDEP ide/ideutils.ml
OCAMLDEP ide/ideproof.ml
OCAMLDEP ide/gtk_parsing.ml
OCAMLDEP ide/coqide_ui.ml
OCAMLDEP ide/coqide.ml
OCAMLDEP ide/coq_commands.ml
OCAMLDEP ide/coq.ml
OCAMLDEP ide/command_windows.ml
OCAMLDEP dev/vm_printers.ml
OCAMLDEP dev/top_printers.ml
OCAMLDEP dev/db_printers.ml
OCAMLDEP config/coq_config.ml
OCAMLDEP checker/validate.ml
OCAMLDEP checker/typeops.ml
OCAMLDEP checker/type_errors.ml
OCAMLDEP checker/term.ml
OCAMLDEP checker/subtyping.ml
OCAMLDEP checker/safe_typing.ml
OCAMLDEP checker/reduction.ml
OCAMLDEP checker/modops.ml
OCAMLDEP checker/mod_checking.ml
OCAMLDEP checker/main.ml
OCAMLDEP checker/inductive.ml
OCAMLDEP checker/indtypes.ml
OCAMLDEP checker/environ.ml
OCAMLDEP checker/declarations.ml
OCAMLDEP checker/closure.ml
OCAMLDEP checker/checker.ml
OCAMLDEP checker/check_stat.ml
OCAMLDEP checker/check.ml
CAMLP4DEPS toplevel/mltop.ml4
CAMLP4DEPS ide/coqide_main.ml4
OCAMLC config/coq_config.mli
OCAMLC config/coq_config.ml
OCAMLC lib/profile.mli
OCAMLC lib/profile.ml
OCAMLC lib/pp_control.mli
OCAMLC lib/pp_control.ml
OCAMLC lib/pp.mli
OCAMLC lib/pp.ml
OCAMLC parsing/tok.mli
OCAMLC lib/compat.ml
OCAMLC lib/flags.mli
OCAMLC lib/flags.ml
OCAMLC lib/segmenttree.mli
OCAMLC lib/segmenttree.ml
OCAMLC lib/unicodetable.ml
OCAMLC lib/util.mli
OCAMLC lib/util.ml
OCAMLC lib/errors.mli
OCAMLC lib/errors.ml
OCAMLC lib/bigint.mli
OCAMLC lib/bigint.ml
OCAMLC lib/dyn.mli
OCAMLC lib/dyn.ml
OCAMLC lib/hashcons.mli
OCAMLC lib/hashcons.ml
OCAMLC lib/predicate.mli
OCAMLC lib/predicate.ml
OCAMLC lib/rtree.mli
OCAMLC lib/rtree.ml
OCAMLC lib/option.mli
OCAMLC lib/option.ml
OCAMLC lib/store.mli
OCAMLC lib/store.ml
OCAMLC lib/hashtbl_alt.mli
OCAMLC lib/hashtbl_alt.ml
OCAMLC kernel/names.mli
OCAMLC kernel/names.ml
OCAMLC kernel/univ.mli
OCAMLC kernel/univ.ml
OCAMLC kernel/esubst.mli
OCAMLC kernel/esubst.ml
OCAMLC kernel/term.mli
OCAMLC kernel/term.ml
OCAMLC kernel/mod_subst.mli
OCAMLC kernel/mod_subst.ml
OCAMLC kernel/sign.mli
OCAMLC kernel/sign.ml
OCAMLC kernel/cbytecodes.mli
OCAMLC kernel/cbytecodes.ml
OCAMLC kernel/copcodes.ml
OCAMLC kernel/cemitcodes.mli
OCAMLC kernel/cemitcodes.ml
OCAMLC kernel/retroknowledge.mli
OCAMLC kernel/declarations.mli
OCAMLC kernel/declarations.ml
OCAMLC kernel/retroknowledge.ml
OCAMLC kernel/pre_env.mli
OCAMLC kernel/pre_env.ml
OCAMLC kernel/cbytegen.mli
OCAMLC kernel/cbytegen.ml
OCAMLC kernel/environ.mli
OCAMLC kernel/environ.ml
OCAMLC kernel/conv_oracle.mli
OCAMLC kernel/conv_oracle.ml
OCAMLC kernel/closure.mli
OCAMLC kernel/closure.ml
OCAMLC kernel/reduction.mli
OCAMLC kernel/reduction.ml
OCAMLC kernel/type_errors.mli
OCAMLC kernel/type_errors.ml
OCAMLC kernel/entries.mli
OCAMLC kernel/entries.ml
OCAMLC kernel/modops.mli
OCAMLC kernel/modops.ml
OCAMLC kernel/inductive.mli
OCAMLC kernel/inductive.ml
OCAMLC kernel/typeops.mli
OCAMLC kernel/typeops.ml
OCAMLC kernel/indtypes.mli
OCAMLC kernel/indtypes.ml
OCAMLC kernel/cooking.mli
OCAMLC kernel/cooking.ml
OCAMLC kernel/term_typing.mli
OCAMLC kernel/term_typing.ml
OCAMLC kernel/subtyping.mli
OCAMLC kernel/subtyping.ml
OCAMLC kernel/mod_typing.mli
OCAMLC kernel/mod_typing.ml
OCAMLC kernel/safe_typing.mli
OCAMLC kernel/safe_typing.ml
OCAMLC library/nameops.mli
OCAMLC library/nameops.ml
OCAMLC library/libnames.mli
OCAMLC library/libnames.ml
OCAMLC library/summary.mli
OCAMLC library/summary.ml
OCAMLC library/nametab.mli
OCAMLC library/nametab.ml
OCAMLC library/libobject.mli
OCAMLC library/libobject.ml
OCAMLC library/lib.mli
OCAMLC library/lib.ml
OCAMLC library/goptionstyp.mli
OCAMLC library/goptions.mli
OCAMLC library/goptions.ml
OCAMLC library/decl_kinds.mli
OCAMLC library/decl_kinds.ml
OCAMLC library/global.mli
OCAMLC library/global.ml
OCAMLC pretyping/termops.mli
OCAMLC pretyping/termops.ml
OCAMLC pretyping/namegen.mli
OCAMLC pretyping/namegen.ml
OCAMLC pretyping/evd.mli
OCAMLC pretyping/evd.ml
OCAMLC pretyping/reductionops.mli
OCAMLC pretyping/reductionops.ml
OCAMLC pretyping/inductiveops.mli
OCAMLC pretyping/inductiveops.ml
OCAMLC pretyping/glob_term.mli
OCAMLC pretyping/glob_term.ml
OCAMLC pretyping/detyping.mli
OCAMLC pretyping/detyping.ml
OCAMLC pretyping/pattern.mli
OCAMLC pretyping/pattern.ml
OCAMLC interp/topconstr.mli
OCAMLC interp/topconstr.ml
OCAMLC interp/ppextend.mli
OCAMLC pretyping/classops.mli
OCAMLC interp/notation.mli
OCAMLC interp/genarg.mli
OCAMLC interp/genarg.ml
OCAMLC interp/ppextend.ml
OCAMLC proofs/tacexpr.ml
OCAMLC parsing/tok.ml
OCAMLC parsing/lexer.mli
OCAMLC parsing/lexer.ml
OCAMLC parsing/extend.mli
OCAMLC parsing/extend.ml
OCAMLC library/declaremods.mli
OCAMLC toplevel/vernacexpr.ml
OCAMLC parsing/extrawit.mli
OCAMLC parsing/extrawit.ml
OCAMLC parsing/pcoq.mli
OCAMLC parsing/pcoq.ml
OCAMLC parsing/q_util.mli
OCAMLC parsing/q_util.ml
OCAMLC parsing/q_coqast.ml
OCAMLC parsing/egrammar.mli
OCAMLC parsing/egrammar.ml
OCAMLC parsing/argextend.ml
OCAMLC parsing/tacextend.ml
OCAMLC parsing/vernacextend.ml
OCAMLC parsing/g_prim.ml
OCAMLC parsing/g_tactic.ml
OCAMLC parsing/g_ltac.ml
OCAMLC parsing/g_constr.ml
Testing parsing/grammar.cma
OCAMLC -a parsing/grammar.cma
CAMLP4O toplevel/whelp.ml4
OCAMLDEP toplevel/whelp.ml
CAMLP4O tactics/tauto.ml4
OCAMLDEP tactics/tauto.ml
CAMLP4O tactics/rewrite.ml4
OCAMLDEP tactics/rewrite.ml
OCAMLC parsing/q_constr.ml
CAMLP4O tactics/hipattern.ml4
OCAMLDEP tactics/hipattern.ml
CAMLP4O tactics/extratactics.ml4
OCAMLDEP tactics/extratactics.ml
CAMLP4O tactics/extraargs.ml4
OCAMLDEP tactics/extraargs.ml
CAMLP4O tactics/eqdecide.ml4
OCAMLDEP tactics/eqdecide.ml
CAMLP4O tactics/eauto.ml4
OCAMLDEP tactics/eauto.ml
CAMLP4O tactics/class_tactics.ml4
OCAMLDEP tactics/class_tactics.ml
CAMLP4O plugins/xml/xmlentries.ml4
OCAMLDEP plugins/xml/xmlentries.ml
CAMLP4O plugins/xml/dumptree.ml4
OCAMLDEP plugins/xml/dumptree.ml
CAMLP4O plugins/subtac/g_subtac.ml4
OCAMLDEP plugins/subtac/g_subtac.ml
CAMLP4O plugins/setoid_ring/newring.ml4
OCAMLDEP plugins/setoid_ring/newring.ml
CAMLP4O plugins/rtauto/g_rtauto.ml4
OCAMLDEP plugins/rtauto/g_rtauto.ml
CAMLP4O plugins/romega/g_romega.ml4
OCAMLDEP plugins/romega/g_romega.ml
CAMLP4O plugins/ring/g_ring.ml4
OCAMLDEP plugins/ring/g_ring.ml
CAMLP4O plugins/quote/g_quote.ml4
OCAMLDEP plugins/quote/g_quote.ml
CAMLP4O plugins/omega/g_omega.ml4
OCAMLDEP plugins/omega/g_omega.ml
CAMLP4O plugins/nsatz/nsatz.ml4
OCAMLDEP plugins/nsatz/nsatz.ml
CAMLP4O plugins/micromega/g_micromega.ml4
OCAMLDEP plugins/micromega/g_micromega.ml
CAMLP4O plugins/funind/g_indfun.ml4
OCAMLDEP plugins/funind/g_indfun.ml
CAMLP4O plugins/fourier/g_fourier.ml4
OCAMLDEP plugins/fourier/g_fourier.ml
CAMLP4O plugins/firstorder/g_ground.ml4
OCAMLDEP plugins/firstorder/g_ground.ml
CAMLP4O plugins/field/field.ml4
OCAMLDEP plugins/field/field.ml
CAMLP4O plugins/extraction/g_extraction.ml4
OCAMLDEP plugins/extraction/g_extraction.ml
CAMLP4O plugins/decl_mode/g_decl_mode.ml4
OCAMLDEP plugins/decl_mode/g_decl_mode.ml
CAMLP4O plugins/cc/g_congruence.ml4
OCAMLDEP plugins/cc/g_congruence.ml
CHECK revision
OCAMLOPT config/coq_config.ml
OCAMLOPT lib/pp_control.ml
OCAMLOPT lib/pp.ml
OCAMLOPT parsing/tok.ml
OCAMLOPT lib/compat.ml
OCAMLOPT lib/flags.ml
OCAMLOPT lib/segmenttree.ml
OCAMLOPT lib/unicodetable.ml
OCAMLOPT lib/util.ml
OCAMLOPT lib/errors.ml
OCAMLC lib/system.mli
OCAMLOPT lib/system.ml
OCAMLC lib/envars.mli
OCAMLOPT lib/envars.ml
OCAMLC scripts/tolink.ml
OCAMLOPT scripts/tolink.ml
OCAMLC scripts/coqmktop.ml
OCAMLOPT scripts/coqmktop.ml
OCAMLOPT -o bin/coqmktop.opt
strip bin/coqmktop.opt
OCAMLC lib/xml_lexer.mli
OCAMLOPT lib/xml_lexer.ml
OCAMLC lib/xml_parser.mli
OCAMLOPT lib/xml_parser.ml
OCAMLC lib/xml_utils.mli
OCAMLOPT lib/xml_utils.ml
OCAMLOPT lib/bigint.ml
OCAMLOPT lib/hashcons.ml
OCAMLOPT lib/dyn.ml
OCAMLC lib/gmap.mli
OCAMLOPT lib/gmap.ml
OCAMLC lib/fset.mli
OCAMLOPT lib/fset.ml
OCAMLC lib/fmap.mli
OCAMLOPT lib/fmap.ml
OCAMLC lib/tries.mli
OCAMLOPT lib/tries.ml
OCAMLC lib/gmapl.mli
OCAMLOPT lib/gmapl.ml
OCAMLOPT lib/profile.ml
OCAMLC lib/explore.mli
OCAMLOPT lib/explore.ml
OCAMLOPT lib/predicate.ml
OCAMLOPT lib/rtree.ml
OCAMLC lib/heap.mli
OCAMLOPT lib/heap.ml
OCAMLOPT lib/option.ml
OCAMLC lib/dnet.mli
OCAMLOPT lib/dnet.ml
OCAMLOPT lib/store.ml
OCAMLC lib/unionfind.mli
OCAMLOPT lib/unionfind.ml
OCAMLOPT lib/hashtbl_alt.ml
OCAMLOPT -a -o lib/lib.cmxa
OCAMLOPT kernel/names.ml
OCAMLOPT kernel/univ.ml
OCAMLOPT kernel/esubst.ml
OCAMLOPT kernel/term.ml
OCAMLOPT kernel/mod_subst.ml
OCAMLOPT kernel/sign.ml
OCAMLOPT kernel/cbytecodes.ml
OCAMLOPT kernel/copcodes.ml
OCAMLOPT kernel/cemitcodes.ml
OCAMLOPT kernel/retroknowledge.ml
OCAMLOPT kernel/declarations.ml
OCAMLOPT kernel/pre_env.ml
OCAMLOPT kernel/cbytegen.ml
OCAMLOPT kernel/environ.ml
OCAMLOPT kernel/conv_oracle.ml
OCAMLOPT kernel/closure.ml
OCAMLOPT kernel/reduction.ml
OCAMLOPT kernel/type_errors.ml
OCAMLOPT kernel/entries.ml
OCAMLOPT kernel/modops.ml
OCAMLOPT kernel/inductive.ml
OCAMLOPT kernel/typeops.ml
OCAMLOPT kernel/indtypes.ml
OCAMLOPT kernel/cooking.ml
OCAMLOPT kernel/term_typing.ml
OCAMLOPT kernel/subtyping.ml
OCAMLOPT kernel/mod_typing.ml
OCAMLOPT kernel/safe_typing.ml
OCAMLC kernel/vm.mli
OCAMLOPT kernel/vm.ml
OCAMLC kernel/csymtable.mli
OCAMLOPT kernel/csymtable.ml
OCAMLC kernel/vconv.mli
OCAMLOPT kernel/vconv.ml
OCAMLOPT -a -o kernel/kernel.cmxa
OCAMLOPT library/nameops.ml
OCAMLOPT library/libnames.ml
OCAMLOPT library/libobject.ml
OCAMLOPT library/summary.ml
OCAMLOPT library/nametab.ml
OCAMLOPT library/global.ml
OCAMLOPT library/lib.ml
OCAMLOPT library/declaremods.ml
OCAMLC library/library.mli
OCAMLOPT library/library.ml
OCAMLC library/states.mli
OCAMLOPT library/states.ml
OCAMLOPT library/decl_kinds.ml
OCAMLC library/dischargedhypsmap.mli
OCAMLOPT library/dischargedhypsmap.ml
OCAMLOPT library/goptions.ml
OCAMLC library/decls.mli
OCAMLOPT library/decls.ml
OCAMLC library/heads.mli
OCAMLOPT library/heads.ml
OCAMLC library/assumptions.mli
OCAMLOPT library/assumptions.ml
OCAMLOPT -a -o library/library.cmxa
OCAMLOPT pretyping/termops.ml
OCAMLOPT pretyping/evd.ml
OCAMLOPT pretyping/reductionops.ml
OCAMLC pretyping/vnorm.mli
OCAMLOPT pretyping/vnorm.ml
OCAMLOPT pretyping/namegen.ml
OCAMLOPT pretyping/inductiveops.ml
OCAMLC pretyping/retyping.mli
OCAMLOPT pretyping/retyping.ml
OCAMLC pretyping/cbv.mli
OCAMLOPT pretyping/cbv.ml
OCAMLOPT pretyping/glob_term.ml
OCAMLC pretyping/pretype_errors.mli
OCAMLOPT pretyping/pretype_errors.ml
OCAMLC pretyping/evarutil.mli
OCAMLOPT pretyping/evarutil.ml
OCAMLC pretyping/term_dnet.mli
OCAMLOPT pretyping/term_dnet.ml
OCAMLC pretyping/recordops.mli
OCAMLOPT pretyping/recordops.ml
OCAMLC pretyping/evarconv.mli
OCAMLOPT pretyping/evarconv.ml
OCAMLC pretyping/arguments_renaming.mli
OCAMLOPT pretyping/arguments_renaming.ml
OCAMLC pretyping/typing.mli
OCAMLOPT pretyping/typing.ml
OCAMLOPT pretyping/pattern.ml
OCAMLC pretyping/matching.mli
OCAMLOPT pretyping/matching.ml
OCAMLC pretyping/tacred.mli
OCAMLOPT pretyping/tacred.ml
OCAMLOPT pretyping/detyping.ml
OCAMLOPT interp/topconstr.ml
OCAMLC pretyping/typeclasses_errors.mli
OCAMLOPT pretyping/typeclasses_errors.ml
OCAMLC pretyping/typeclasses.mli
OCAMLOPT pretyping/typeclasses.ml
OCAMLOPT pretyping/classops.ml
OCAMLC pretyping/coercion.mli
OCAMLOPT pretyping/coercion.ml
OCAMLC pretyping/unification.mli
OCAMLOPT pretyping/unification.ml
OCAMLC pretyping/indrec.mli
OCAMLOPT pretyping/indrec.ml
OCAMLC pretyping/cases.mli
OCAMLOPT pretyping/cases.ml
OCAMLC pretyping/pretyping.mli
OCAMLOPT pretyping/pretyping.ml
OCAMLOPT -a -o pretyping/pretyping.cmxa
OCAMLOPT parsing/lexer.ml
OCAMLOPT interp/ppextend.ml
OCAMLOPT interp/notation.ml
OCAMLC interp/dumpglob.mli
OCAMLOPT interp/dumpglob.ml
OCAMLOPT interp/genarg.ml
OCAMLC interp/syntax_def.mli
OCAMLOPT interp/syntax_def.ml
OCAMLC interp/smartlocate.mli
OCAMLOPT interp/smartlocate.ml
OCAMLC interp/reserve.mli
OCAMLOPT interp/reserve.ml
OCAMLC library/impargs.mli
OCAMLOPT library/impargs.ml
OCAMLC interp/implicit_quantifiers.mli
OCAMLOPT interp/implicit_quantifiers.ml
OCAMLC interp/constrintern.mli
OCAMLOPT interp/constrintern.ml
OCAMLC interp/modintern.mli
OCAMLOPT interp/modintern.ml
OCAMLC interp/constrextern.mli
OCAMLOPT interp/constrextern.ml
OCAMLC interp/coqlib.mli
OCAMLOPT interp/coqlib.ml
OCAMLC toplevel/discharge.mli
OCAMLOPT toplevel/discharge.ml
OCAMLC library/declare.mli
OCAMLOPT library/declare.ml
OCAMLOPT -a -o interp/interp.cmxa
OCAMLC proofs/goal.mli
OCAMLOPT proofs/goal.ml
OCAMLOPT proofs/tacexpr.ml
OCAMLC proofs/proof_type.mli
OCAMLOPT proofs/proof_type.ml
OCAMLC proofs/logic.mli
OCAMLOPT proofs/logic.ml
OCAMLC proofs/refiner.mli
OCAMLOPT proofs/refiner.ml
OCAMLC proofs/evar_refiner.mli
OCAMLOPT proofs/evar_refiner.ml
OCAMLC proofs/proofview.mli
OCAMLOPT proofs/proofview.ml
OCAMLC proofs/proof.mli
OCAMLOPT proofs/proof.ml
OCAMLOPT parsing/extend.ml
OCAMLOPT toplevel/vernacexpr.ml
OCAMLC proofs/proof_global.mli
OCAMLOPT proofs/proof_global.ml
OCAMLC proofs/redexpr.mli
OCAMLOPT proofs/redexpr.ml
OCAMLC proofs/tacmach.mli
OCAMLOPT proofs/tacmach.ml
OCAMLC proofs/pfedit.mli
OCAMLOPT proofs/pfedit.ml
OCAMLC proofs/tactic_debug.mli
OCAMLOPT proofs/tactic_debug.ml
OCAMLC proofs/clenv.mli
OCAMLOPT proofs/clenv.ml
OCAMLC proofs/clenvtac.mli
OCAMLOPT proofs/clenvtac.ml
OCAMLOPT -a -o proofs/proofs.cmxa
OCAMLOPT parsing/extrawit.ml
OCAMLOPT parsing/pcoq.ml
OCAMLOPT parsing/egrammar.ml
OCAMLC parsing/g_xml.ml
OCAMLOPT parsing/g_xml.ml
OCAMLC parsing/ppconstr.mli
OCAMLOPT parsing/ppconstr.ml
OCAMLC parsing/printer.mli
OCAMLOPT parsing/printer.ml
OCAMLC parsing/pptactic.mli
OCAMLOPT parsing/pptactic.ml
OCAMLC parsing/tactic_printer.mli
OCAMLOPT parsing/tactic_printer.ml
OCAMLC parsing/printmod.mli
OCAMLOPT parsing/printmod.ml
OCAMLC parsing/prettyp.mli
OCAMLOPT parsing/prettyp.ml
OCAMLOPT -a -o parsing/parsing.cmxa
OCAMLC tactics/dn.mli
OCAMLOPT tactics/dn.ml
OCAMLC tactics/termdn.mli
OCAMLOPT tactics/termdn.ml
OCAMLC tactics/btermdn.mli
OCAMLOPT tactics/btermdn.ml
OCAMLC tactics/nbtermdn.mli
OCAMLOPT tactics/nbtermdn.ml
OCAMLC tactics/tacticals.mli
OCAMLOPT tactics/tacticals.ml
OCAMLC tactics/hipattern.mli
OCAMLOPT tactics/hipattern.ml
OCAMLC toplevel/ind_tables.mli
OCAMLOPT toplevel/ind_tables.ml
OCAMLC tactics/eqschemes.mli
OCAMLOPT tactics/eqschemes.ml
OCAMLC tactics/elimschemes.mli
OCAMLOPT tactics/elimschemes.ml
OCAMLC tactics/tactics.mli
OCAMLOPT tactics/tactics.ml
OCAMLC tactics/hiddentac.mli
OCAMLOPT tactics/hiddentac.ml
OCAMLC tactics/elim.mli
OCAMLOPT tactics/elim.ml
OCAMLC tactics/auto.mli
OCAMLOPT tactics/auto.ml
OCAMLC tactics/equality.mli
OCAMLOPT tactics/equality.ml
OCAMLC tactics/contradiction.mli
OCAMLOPT tactics/contradiction.ml
OCAMLC tactics/inv.mli
OCAMLOPT tactics/inv.ml
OCAMLC tactics/leminv.mli
OCAMLOPT tactics/leminv.ml
OCAMLC tactics/tacinterp.mli
OCAMLOPT tactics/tacinterp.ml
OCAMLC tactics/evar_tactics.mli
OCAMLOPT tactics/evar_tactics.ml
OCAMLC toplevel/himsg.mli
OCAMLOPT toplevel/himsg.ml
OCAMLC toplevel/vernacinterp.mli
OCAMLOPT toplevel/vernacinterp.ml
OCAMLC tactics/autorewrite.mli
OCAMLOPT tactics/autorewrite.ml
OCAMLC tactics/tactic_option.mli
OCAMLOPT tactics/tactic_option.ml
OCAMLOPT -a -o tactics/tactics.cmxa
OCAMLC toplevel/cerrors.mli
OCAMLOPT toplevel/cerrors.ml
OCAMLC toplevel/class.mli
OCAMLOPT toplevel/class.ml
OCAMLC toplevel/metasyntax.mli
OCAMLOPT toplevel/metasyntax.ml
OCAMLC toplevel/auto_ind_decl.mli
OCAMLOPT toplevel/auto_ind_decl.ml
OCAMLC toplevel/libtypes.mli
OCAMLOPT toplevel/libtypes.ml
OCAMLC toplevel/search.mli
OCAMLOPT toplevel/search.ml
OCAMLC toplevel/autoinstance.mli
OCAMLOPT toplevel/autoinstance.ml
OCAMLC toplevel/lemmas.mli
OCAMLOPT toplevel/lemmas.ml
OCAMLC toplevel/indschemes.mli
OCAMLOPT toplevel/indschemes.ml
OCAMLC toplevel/command.mli
OCAMLOPT toplevel/command.ml
OCAMLC toplevel/classes.mli
OCAMLOPT toplevel/classes.ml
OCAMLC toplevel/record.mli
OCAMLOPT toplevel/record.ml
OCAMLC parsing/ppvernac.mli
OCAMLOPT parsing/ppvernac.ml
OCAMLC toplevel/backtrack.mli
OCAMLOPT toplevel/backtrack.ml
CAMLP4O toplevel/mltop.ml4
OCAMLC toplevel/mltop.mli
OCAMLOPT toplevel/mltop.optml
OCAMLC toplevel/vernacentries.mli
OCAMLOPT toplevel/vernacentries.ml
OCAMLC toplevel/whelp.mli
OCAMLOPT toplevel/whelp.ml
OCAMLC toplevel/vernac.mli
OCAMLOPT toplevel/vernac.ml
OCAMLC toplevel/interface.mli
OCAMLC toplevel/ide_intf.mli
OCAMLOPT toplevel/ide_intf.ml
OCAMLC toplevel/ide_slave.mli
OCAMLOPT toplevel/ide_slave.ml
OCAMLC toplevel/toplevel.mli
OCAMLOPT toplevel/toplevel.ml
OCAMLC toplevel/usage.mli
OCAMLOPT toplevel/usage.ml
OCAMLC toplevel/coqinit.mli
OCAMLOPT toplevel/coqinit.ml
OCAMLC toplevel/coqtop.mli
OCAMLOPT toplevel/coqtop.ml
OCAMLOPT -a -o toplevel/toplevel.cmxa
OCAMLOPT parsing/g_constr.ml
OCAMLC parsing/g_vernac.ml
OCAMLOPT parsing/g_vernac.ml
OCAMLOPT parsing/g_prim.ml
OCAMLC parsing/g_proofs.ml
OCAMLOPT parsing/g_proofs.ml
OCAMLOPT parsing/g_tactic.ml
OCAMLOPT parsing/g_ltac.ml
OCAMLOPT -a -o parsing/highparsing.cmxa
OCAMLC tactics/refine.mli
OCAMLOPT tactics/refine.ml
OCAMLC tactics/extraargs.mli
OCAMLOPT tactics/extraargs.ml
OCAMLC tactics/extratactics.mli
OCAMLOPT tactics/extratactics.ml
OCAMLC tactics/eauto.mli
OCAMLOPT tactics/eauto.ml
OCAMLC tactics/class_tactics.ml
OCAMLOPT tactics/class_tactics.ml
OCAMLC tactics/rewrite.ml
OCAMLOPT tactics/rewrite.ml
OCAMLC tactics/tauto.ml
OCAMLOPT tactics/tauto.ml
OCAMLC tactics/eqdecide.ml
OCAMLOPT tactics/eqdecide.ml
OCAMLOPT -a -o tactics/hightactics.cmxa
OCAMLC kernel/byterun/coq_fix_code.c
OCAMLC kernel/byterun/coq_memory.c
OCAMLC kernel/byterun/coq_values.c
OCAMLC kernel/byterun/coq_interp.c
cd kernel/byterun/ && \
"ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
COQMKTOP -o bin/coqtop.opt
strip bin/coqtop.opt
COQC -nois theories/Init/Notations.v
COQC -nois theories/Init/Logic.v
Identifier 'IF' now a keyword
Identifier 'exists2' now a keyword
Identifier 'rew' now a keyword
OCAMLC plugins/syntax/nat_syntax.ml
OCAMLC plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLC -a -o plugins/syntax/nat_syntax_plugin.cma
OCAMLOPT plugins/syntax/nat_syntax.ml
OCAMLOPT plugins/syntax/nat_syntax_plugin_mod.ml
OCAMLOPT -a -o plugins/syntax/nat_syntax_plugin.cmxa
OCAMLOPT -shared -o plugins/syntax/nat_syntax_plugin.cmxs
COQC -nois theories/Init/Datatypes.v
File "/private/tmp/homebrew-coq-8.4-dzw8/coq-8.4/theories/Init/Datatypes.v", line 13, characters 0-38:
Error: error loading shared library: dlopen(/private/tmp/homebrew-coq-8.4-dzw8/coq-8.4/plugins/syntax/nat_syntax_plugin.cmxs, 138): Symbol not found: _camlBigint
Referenced from: /private/tmp/homebrew-coq-8.4-dzw8/coq-8.4/plugins/syntax/nat_syntax_plugin.cmxs
Expected in: flat namespace
in /private/tmp/homebrew-coq-8.4-dzw8/coq-8.4/plugins/syntax/nat_syntax_plugin.cmxs
==> Exit Status: 2
https://github.com/mxcl/master/blob/master/Library/Formula/coq.rb#L44
==> Build Environment
HOMEBREW_VERSION: 0.9.2
HEAD: 5b1ac77d74b43bd3e9ff30d1a906f7123f1e665f
CPU: dual-core 64-bit penryn
OS X: 10.7.4-x86_64
Xcode: 4.4.1
CLT: 4.4.0.0.1.1249367152
X11: 2.6.4 in /usr/X11
CC: /usr/bin/clang
CXX: /usr/bin/clang++ => /usr/bin/clang
LD: /usr/bin/clang
CFLAGS: -Os -w -pipe -march=native -Qunused-arguments -mmacosx-version-min=10.7
CXXFLAGS: -Os -w -pipe -march=native -Qunused-arguments -mmacosx-version-min=10.7
LDFLAGS: -L/usr/local/lib
MACOSX_DEPLOYMENT_TARGET: 10.7
HOMEBREW_MAKE_JOBS: 1
OBJC: /usr/bin/clang
PATH: /usr/local/share/python:/usr/local/bin:/usr/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/usr/local/bin:/usr/X11/bin:/usr/local/git/bin:/Users/kenn/.rvm/bin:/usr/local/Library/Contributions/cmds
Error: Failed executing: make world (coq.rb:44)
This link will help resolve the above errors:
https://github.com/mxcl/homebrew/wiki/bug-fixing-checklist
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment