Created
August 29, 2012 16:54
-
-
Save kennknowles/3515580 to your computer and use it in GitHub Desktop.
brew install coq
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ==> 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