Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- You have GNU Make 4.1. Good!
- You have Objective-Caml 4.02.1. Good!
- You have native-code compilation. Good!
- LablGtk2 found in ocaml lib directory, native threads: native CoqIde will be available.
- Coq top directory : /home/thorsten/tmp.aur/coq/src/coq-8.4pl5
- Architecture : Linux
- Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/usr/lib/coq'
- Coq tools bytecode link flags :
- OS dependent libraries : -cclib -lunix
- Objective-Caml/Camlp4 version : 4.02.1
- Objective-Caml/Camlp4 binaries in : /usr/bin
- Objective-Caml library in : /usr/lib/ocaml
- Camlp4 library in : +camlp4
- Native dynamic link support : true
- Lablgtk2 library in : +lablgtk2
- Documentation : None
- CoqIde : opt
- 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/bin
- library will be copied in /usr/lib/coq
- config files will be copied in /etc/xdg/coq/
- data files will be copied in /usr/share/coq
- man pages will be copied in /usr/share/man
- documentation will be copied in /usr/share/doc/coq
- emacs mode will be copied in /usr/share/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 --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
- make[1]: Entering directory '/home/thorsten/tmp.aur/coq/src/coq-8.4pl5'
- OCAMLLEX tools/coqdep_lexer.mll
- 348 states, 7127 transitions, table size 30596 bytes
- 3131 additional bytes used for bindings
- OCAMLBEST -o bin/coqdep_boot
- File "tools/coqdep_common.ml", line 268, characters 17-19:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 268, characters 28-30:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 269, characters 1-3:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 270, characters 1-3:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 270, characters 12-14:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 270, characters 23-25:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 270, characters 34-36:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- File "tools/coqdep_common.ml", line 271, characters 1-3:
- Warning 3: deprecated: Pervasives.or
- Use (||) instead.
- "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/utf8_convert.mll
- 15 states, 827 transitions, table size 3398 bytes
- OCAMLLEX ide/config_lexer.mll
- 30 states, 1657 transitions, table size 6808 bytes
- 6096 additional bytes used for bindings
- OCAMLLEX ide/coq_lex.mll
- ocamllex warning:
- File "ide/coq_lex.mll", line 112, character 66: unescaped newline in string.
- 454 states, 31913 transitions, table size 130376 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
- OCAMLLEX tools/coqdoc/cpretty.mll
- 2472 states, 7945 transitions, table size 46612 bytes
- OCAMLLEX lib/xml_lexer.mll
- 78 states, 800 transitions, table size 3668 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/omega/omega_plugin_mod.ml
- ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
- ECHO... > plugins/fourier/fourier_plugin_mod.ml
- ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
- ECHO... > plugins/funind/recdef_plugin_mod.ml
- ECHO... > plugins/micromega/micromega_plugin_mod.ml
- ECHO... > plugins/xml/xml_plugin_mod.ml
- ECHO... > plugins/subtac/subtac_plugin_mod.ml
- ECHO... > plugins/quote/quote_plugin_mod.ml
- ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
- ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
- ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
- ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
- ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
- ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
- ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
- ECHO... > plugins/firstorder/ground_plugin_mod.ml
- ECHO... > plugins/field/field_plugin_mod.ml
- ECHO... > plugins/extraction/extraction_plugin_mod.ml
- ECHO... > plugins/cc/cc_plugin_mod.ml
- ECHO... > plugins/romega/romega_plugin_mod.ml
- ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml
- ECHO... > plugins/ring/ring_plugin_mod.ml
- COQDEP parsing/grammar.mllib
- COQDEP parsing/parsing.mllib
- COQDEP parsing/highparsing.mllib
- COQDEP lib/lib.mllib
- COQDEP tactics/tactics.mllib
- COQDEP tactics/hightactics.mllib
- COQDEP proofs/proofs.mllib
- COQDEP tools/win32hack.mllib
- COQDEP toplevel/toplevel.mllib
- COQDEP checker/check.mllib
- COQDEP pretyping/pretyping.mllib
- COQDEP interp/interp.mllib
- COQDEP kernel/kernel.mllib
- COQDEP ide/ide.mllib
- COQDEP library/library.mllib
- COQDEP dev/printers.mllib
- COQDEP plugins/ring/ring_plugin.mllib
- COQDEP plugins/decl_mode/decl_mode_plugin.mllib
- COQDEP plugins/romega/romega_plugin.mllib
- COQDEP plugins/cc/cc_plugin.mllib
- COQDEP plugins/extraction/extraction_plugin.mllib
- COQDEP plugins/field/field_plugin.mllib
- COQDEP plugins/firstorder/ground_plugin.mllib
- COQDEP plugins/syntax/z_syntax_plugin.mllib
- COQDEP plugins/syntax/numbers_syntax_plugin.mllib
- COQDEP plugins/syntax/nat_syntax_plugin.mllib
- COQDEP plugins/syntax/string_syntax_plugin.mllib
- COQDEP plugins/syntax/ascii_syntax_plugin.mllib
- COQDEP plugins/syntax/r_syntax_plugin.mllib
- COQDEP plugins/setoid_ring/newring_plugin.mllib
- COQDEP plugins/quote/quote_plugin.mllib
- COQDEP plugins/subtac/subtac_plugin.mllib
- COQDEP plugins/xml/xml_plugin.mllib
- COQDEP plugins/micromega/micromega_plugin.mllib
- COQDEP plugins/funind/recdef_plugin.mllib
- COQDEP plugins/nsatz/nsatz_plugin.mllib
- COQDEP plugins/fourier/fourier_plugin.mllib
- COQDEP plugins/rtauto/rtauto_plugin.mllib
- COQDEP plugins/omega/omega_plugin.mllib
- CCDEP kernel/byterun/coq_memory.c
- CCDEP kernel/byterun/coq_values.c
- CCDEP kernel/byterun/coq_fix_code.c
- CCDEP kernel/byterun/coq_interp.c
- CCDEP ide/ide_win32_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/undo.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/ring/ring_plugin_mod.ml
- OCAMLDEP plugins/decl_mode/decl_mode_plugin_mod.ml
- OCAMLDEP plugins/romega/romega_plugin_mod.ml
- OCAMLDEP plugins/cc/cc_plugin_mod.ml
- OCAMLDEP plugins/extraction/extraction_plugin_mod.ml
- OCAMLDEP plugins/field/field_plugin_mod.ml
- OCAMLDEP plugins/firstorder/ground_plugin_mod.ml
- OCAMLDEP plugins/syntax/z_syntax_plugin_mod.ml
- OCAMLDEP plugins/syntax/numbers_syntax_plugin_mod.ml
- OCAMLDEP plugins/syntax/nat_syntax_plugin_mod.ml
- OCAMLDEP plugins/syntax/string_syntax_plugin_mod.ml
- OCAMLDEP plugins/syntax/ascii_syntax_plugin_mod.ml
- OCAMLDEP plugins/syntax/r_syntax_plugin_mod.ml
- OCAMLDEP plugins/setoid_ring/newring_plugin_mod.ml
- OCAMLDEP plugins/quote/quote_plugin_mod.ml
- OCAMLDEP plugins/subtac/subtac_plugin_mod.ml
- OCAMLDEP plugins/xml/xml_plugin_mod.ml
- OCAMLDEP plugins/micromega/micromega_plugin_mod.ml
- OCAMLDEP plugins/funind/recdef_plugin_mod.ml
- OCAMLDEP plugins/nsatz/nsatz_plugin_mod.ml
- OCAMLDEP plugins/fourier/fourier_plugin_mod.ml
- OCAMLDEP plugins/rtauto/rtauto_plugin_mod.ml
- OCAMLDEP plugins/omega/omega_plugin_mod.ml
- "ocamlc.opt" -rectypes -c -I "+camlp4" -pp 'camlp4orf -impl' -impl tools/compat5.mlp
- File "tools/compat5.mlp", line 1:
- Error: The files /usr/lib/ocaml/pervasives.cmi
- and /usr/lib/ocaml/camlp4/Camlp4.cmi make inconsistent assumptions
- over interface Pervasives
- Makefile.build:563: recipe for target 'tools/compat5.cmo' failed
- make[1]: *** [tools/compat5.cmo] Error 2
- make[1]: Leaving directory '/home/thorsten/tmp.aur/coq/src/coq-8.4pl5'
- Makefile:139: recipe for target 'world' failed
- make: *** [world] Error 2
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement