API tools faq
paste
Advertisement
Guest User

Coq build failure on archlinux with ocaml 4.02.1

a guest
Dec 22nd, 2014
379
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 37.44 KB | None | 0 0
raw download clone embed print report
  1. You have GNU Make 4.1. Good!
  2. You have Objective-Caml 4.02.1. Good!
  3. You have native-code compilation. Good!
  4. LablGtk2 found in ocaml lib directory, native threads: native CoqIde will be available.
  5.  
  6. Coq top directory : /home/thorsten/tmp.aur/coq/src/coq-8.4pl5
  7. Architecture : Linux
  8. Coq VM bytecode link flags : -dllib -lcoqrun -dllpath '/usr/lib/coq'
  9. Coq tools bytecode link flags :
  10. OS dependent libraries : -cclib -lunix
  11. Objective-Caml/Camlp4 version : 4.02.1
  12. Objective-Caml/Camlp4 binaries in : /usr/bin
  13. Objective-Caml library in : /usr/lib/ocaml
  14. Camlp4 library in : +camlp4
  15. Native dynamic link support : true
  16. Lablgtk2 library in : +lablgtk2
  17. Documentation : None
  18. CoqIde : opt
  19. Web browser : firefox -remote "OpenURL(%s,new-tab)" || firefox %s &
  20. Coq web site : http://coq.inria.fr/
  21.  
  22. Paths for true installation:
  23. binaries will be copied in /usr/bin
  24. library will be copied in /usr/lib/coq
  25. config files will be copied in /etc/xdg/coq/
  26. data files will be copied in /usr/share/coq
  27. man pages will be copied in /usr/share/man
  28. documentation will be copied in /usr/share/doc/coq
  29. emacs mode will be copied in /usr/share/emacs/site-lisp
  30.  
  31. If anything in the above is wrong, please restart './configure'.
  32.  
  33. *Warning* To compile the system for a new architecture
  34. don't forget to do a 'make archclean' before './configure'.
  35. make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
  36. make[1]: Entering directory '/home/thorsten/tmp.aur/coq/src/coq-8.4pl5'
  37. OCAMLLEX tools/coqdep_lexer.mll
  38. 348 states, 7127 transitions, table size 30596 bytes
  39. 3131 additional bytes used for bindings
  40. OCAMLBEST -o bin/coqdep_boot
  41. File "tools/coqdep_common.ml", line 268, characters 17-19:
  42. Warning 3: deprecated: Pervasives.or
  43. Use (||) instead.
  44. File "tools/coqdep_common.ml", line 268, characters 28-30:
  45. Warning 3: deprecated: Pervasives.or
  46. Use (||) instead.
  47. File "tools/coqdep_common.ml", line 269, characters 1-3:
  48. Warning 3: deprecated: Pervasives.or
  49. Use (||) instead.
  50. File "tools/coqdep_common.ml", line 270, characters 1-3:
  51. Warning 3: deprecated: Pervasives.or
  52. Use (||) instead.
  53. File "tools/coqdep_common.ml", line 270, characters 12-14:
  54. Warning 3: deprecated: Pervasives.or
  55. Use (||) instead.
  56. File "tools/coqdep_common.ml", line 270, characters 23-25:
  57. Warning 3: deprecated: Pervasives.or
  58. Use (||) instead.
  59. File "tools/coqdep_common.ml", line 270, characters 34-36:
  60. Warning 3: deprecated: Pervasives.or
  61. Use (||) instead.
  62. File "tools/coqdep_common.ml", line 271, characters 1-3:
  63. Warning 3: deprecated: Pervasives.or
  64. Use (||) instead.
  65. "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})
  66. COQDEP plugins/extraction/ExtrOcamlString.v
  67. COQDEP plugins/extraction/ExtrOcamlZBigInt.v
  68. COQDEP plugins/extraction/ExtrOcamlZInt.v
  69. COQDEP plugins/extraction/ExtrOcamlNatBigInt.v
  70. COQDEP plugins/extraction/ExtrOcamlNatInt.v
  71. COQDEP plugins/extraction/ExtrOcamlBigIntConv.v
  72. COQDEP plugins/extraction/ExtrOcamlIntConv.v
  73. COQDEP plugins/extraction/ExtrOcamlBasic.v
  74. COQDEP plugins/nsatz/Nsatz.v
  75. COQDEP plugins/quote/Quote.v
  76. COQDEP plugins/setoid_ring/Integral_domain.v
  77. COQDEP plugins/setoid_ring/Rings_Q.v
  78. COQDEP plugins/setoid_ring/Rings_R.v
  79. COQDEP plugins/setoid_ring/Rings_Z.v
  80. COQDEP plugins/setoid_ring/Ncring_tac.v
  81. COQDEP plugins/setoid_ring/Ncring_initial.v
  82. COQDEP plugins/setoid_ring/Ncring_polynom.v
  83. COQDEP plugins/setoid_ring/Ncring.v
  84. COQDEP plugins/setoid_ring/Cring.v
  85. COQDEP plugins/setoid_ring/Algebra_syntax.v
  86. COQDEP plugins/setoid_ring/ZArithRing.v
  87. COQDEP plugins/setoid_ring/Ring.v
  88. COQDEP plugins/setoid_ring/Ring_theory.v
  89. COQDEP plugins/setoid_ring/Ring_tac.v
  90. COQDEP plugins/setoid_ring/Ring_polynom.v
  91. COQDEP plugins/setoid_ring/Ring_equiv.v
  92. COQDEP plugins/setoid_ring/Ring_base.v
  93. COQDEP plugins/setoid_ring/RealField.v
  94. COQDEP plugins/setoid_ring/NArithRing.v
  95. COQDEP plugins/setoid_ring/InitialRing.v
  96. COQDEP plugins/setoid_ring/Field.v
  97. COQDEP plugins/setoid_ring/Field_theory.v
  98. COQDEP plugins/setoid_ring/Field_tac.v
  99. COQDEP plugins/setoid_ring/BinList.v
  100. COQDEP plugins/setoid_ring/ArithRing.v
  101. COQDEP plugins/rtauto/Rtauto.v
  102. COQDEP plugins/rtauto/Bintree.v
  103. COQDEP plugins/funind/Recdef.v
  104. COQDEP plugins/fourier/Fourier.v
  105. COQDEP plugins/fourier/Fourier_util.v
  106. COQDEP plugins/field/LegacyField.v
  107. COQDEP plugins/field/LegacyField_Theory.v
  108. COQDEP plugins/field/LegacyField_Tactic.v
  109. COQDEP plugins/field/LegacyField_Compl.v
  110. COQDEP plugins/ring/Setoid_ring.v
  111. COQDEP plugins/ring/Setoid_ring_theory.v
  112. COQDEP plugins/ring/Setoid_ring_normalize.v
  113. COQDEP plugins/ring/Ring_normalize.v
  114. COQDEP plugins/ring/Ring_abstract.v
  115. COQDEP plugins/ring/LegacyZArithRing.v
  116. COQDEP plugins/ring/LegacyRing.v
  117. COQDEP plugins/ring/LegacyRing_theory.v
  118. COQDEP plugins/ring/LegacyNArithRing.v
  119. COQDEP plugins/ring/LegacyArithRing.v
  120. COQDEP plugins/micromega/ZMicromega.v
  121. COQDEP plugins/micromega/ZCoeff.v
  122. COQDEP plugins/micromega/VarMap.v
  123. COQDEP plugins/micromega/Tauto.v
  124. COQDEP plugins/micromega/RMicromega.v
  125. COQDEP plugins/micromega/RingMicromega.v
  126. COQDEP plugins/micromega/Refl.v
  127. COQDEP plugins/micromega/QMicromega.v
  128. COQDEP plugins/micromega/Psatz.v
  129. COQDEP plugins/micromega/OrderedRing.v
  130. COQDEP plugins/micromega/Env.v
  131. COQDEP plugins/micromega/EnvRing.v
  132. COQDEP plugins/micromega/CheckerMaker.v
  133. COQDEP plugins/romega/ROmega.v
  134. COQDEP plugins/romega/ReflOmegaCore.v
  135. COQDEP plugins/omega/PreOmega.v
  136. COQDEP plugins/omega/Omega.v
  137. COQDEP plugins/omega/OmegaPlugin.v
  138. COQDEP plugins/omega/OmegaLemmas.v
  139. COQDEP theories/Vectors/Vector.v
  140. COQDEP theories/Vectors/VectorSpec.v
  141. COQDEP theories/Vectors/VectorDef.v
  142. COQDEP theories/Vectors/Fin.v
  143. COQDEP theories/Structures/OrderedType.v
  144. COQDEP theories/Structures/OrderedTypeEx.v
  145. COQDEP theories/Structures/OrderedTypeAlt.v
  146. COQDEP theories/Structures/DecidableTypeEx.v
  147. COQDEP theories/Structures/DecidableType.v
  148. COQDEP theories/Structures/GenericMinMax.v
  149. COQDEP theories/Structures/OrdersAlt.v
  150. COQDEP theories/Structures/OrdersTac.v
  151. COQDEP theories/Structures/OrdersLists.v
  152. COQDEP theories/Structures/OrdersFacts.v
  153. COQDEP theories/Structures/OrdersEx.v
  154. COQDEP theories/Structures/Orders.v
  155. COQDEP theories/Structures/EqualitiesFacts.v
  156. COQDEP theories/Structures/Equalities.v
  157. COQDEP theories/Program/Wf.v
  158. COQDEP theories/Program/Utils.v
  159. COQDEP theories/Program/Tactics.v
  160. COQDEP theories/Program/Syntax.v
  161. COQDEP theories/Program/Subset.v
  162. COQDEP theories/Program/Program.v
  163. COQDEP theories/Program/Equality.v
  164. COQDEP theories/Program/Combinators.v
  165. COQDEP theories/Program/Basics.v
  166. COQDEP theories/Classes/RelationPairs.v
  167. COQDEP theories/Classes/SetoidTactics.v
  168. COQDEP theories/Classes/SetoidDec.v
  169. COQDEP theories/Classes/SetoidClass.v
  170. COQDEP theories/Classes/RelationClasses.v
  171. COQDEP theories/Classes/Morphisms.v
  172. COQDEP theories/Classes/Morphisms_Relations.v
  173. COQDEP theories/Classes/Morphisms_Prop.v
  174. COQDEP theories/Classes/Init.v
  175. COQDEP theories/Classes/EquivDec.v
  176. COQDEP theories/Classes/Equivalence.v
  177. COQDEP theories/Unicode/Utf8_core.v
  178. COQDEP theories/Unicode/Utf8.v
  179. COQDEP theories/Numbers/Rational/SpecViaQ/QSig.v
  180. COQDEP theories/Numbers/Rational/BigQ/QMake.v
  181. COQDEP theories/Numbers/Rational/BigQ/BigQ.v
  182. COQDEP theories/Numbers/NumPrelude.v
  183. COQDEP theories/Numbers/Natural/SpecViaZ/NSig.v
  184. COQDEP theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
  185. COQDEP theories/Numbers/Natural/Peano/NPeano.v
  186. COQDEP theories/Numbers/Natural/Binary/NBinary.v
  187. COQDEP theories/Numbers/Natural/BigN/NMake.v
  188. COQDEP theories/Numbers/Natural/BigN/NMake_gen.v
  189. COQDEP theories/Numbers/Natural/BigN/Nbasic.v
  190. COQDEP theories/Numbers/Natural/BigN/BigN.v
  191. COQDEP theories/Numbers/Natural/Abstract/NBits.v
  192. COQDEP theories/Numbers/Natural/Abstract/NLcm.v
  193. COQDEP theories/Numbers/Natural/Abstract/NGcd.v
  194. COQDEP theories/Numbers/Natural/Abstract/NLog.v
  195. COQDEP theories/Numbers/Natural/Abstract/NSqrt.v
  196. COQDEP theories/Numbers/Natural/Abstract/NPow.v
  197. COQDEP theories/Numbers/Natural/Abstract/NParity.v
  198. COQDEP theories/Numbers/Natural/Abstract/NMaxMin.v
  199. COQDEP theories/Numbers/Natural/Abstract/NDiv.v
  200. COQDEP theories/Numbers/Natural/Abstract/NProperties.v
  201. COQDEP theories/Numbers/Natural/Abstract/NSub.v
  202. COQDEP theories/Numbers/Natural/Abstract/NStrongRec.v
  203. COQDEP theories/Numbers/Natural/Abstract/NOrder.v
  204. COQDEP theories/Numbers/Natural/Abstract/NMulOrder.v
  205. COQDEP theories/Numbers/Natural/Abstract/NIso.v
  206. COQDEP theories/Numbers/Natural/Abstract/NDefOps.v
  207. COQDEP theories/Numbers/Natural/Abstract/NBase.v
  208. COQDEP theories/Numbers/Natural/Abstract/NAxioms.v
  209. COQDEP theories/Numbers/Natural/Abstract/NAdd.v
  210. COQDEP theories/Numbers/Natural/Abstract/NAddOrder.v
  211. COQDEP theories/Numbers/NatInt/NZBits.v
  212. COQDEP theories/Numbers/NatInt/NZGcd.v
  213. COQDEP theories/Numbers/NatInt/NZLog.v
  214. COQDEP theories/Numbers/NatInt/NZSqrt.v
  215. COQDEP theories/Numbers/NatInt/NZPow.v
  216. COQDEP theories/Numbers/NatInt/NZDiv.v
  217. COQDEP theories/Numbers/NatInt/NZParity.v
  218. COQDEP theories/Numbers/NatInt/NZDomain.v
  219. COQDEP theories/Numbers/NatInt/NZProperties.v
  220. COQDEP theories/Numbers/NatInt/NZOrder.v
  221. COQDEP theories/Numbers/NatInt/NZMul.v
  222. COQDEP theories/Numbers/NatInt/NZMulOrder.v
  223. COQDEP theories/Numbers/NatInt/NZBase.v
  224. COQDEP theories/Numbers/NatInt/NZAxioms.v
  225. COQDEP theories/Numbers/NatInt/NZAdd.v
  226. COQDEP theories/Numbers/NatInt/NZAddOrder.v
  227. COQDEP theories/Numbers/NaryFunctions.v
  228. COQDEP theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
  229. COQDEP theories/Numbers/Integer/SpecViaZ/ZSig.v
  230. COQDEP theories/Numbers/Integer/NatPairs/ZNatPairs.v
  231. COQDEP theories/Numbers/Integer/Binary/ZBinary.v
  232. COQDEP theories/Numbers/Integer/BigZ/ZMake.v
  233. COQDEP theories/Numbers/Integer/BigZ/BigZ.v
  234. COQDEP theories/Numbers/Integer/Abstract/ZProperties.v
  235. COQDEP theories/Numbers/Integer/Abstract/ZBits.v
  236. COQDEP theories/Numbers/Integer/Abstract/ZLcm.v
  237. COQDEP theories/Numbers/Integer/Abstract/ZGcd.v
  238. COQDEP theories/Numbers/Integer/Abstract/ZPow.v
  239. COQDEP theories/Numbers/Integer/Abstract/ZParity.v
  240. COQDEP theories/Numbers/Integer/Abstract/ZMaxMin.v
  241. COQDEP theories/Numbers/Integer/Abstract/ZDivEucl.v
  242. COQDEP theories/Numbers/Integer/Abstract/ZDivTrunc.v
  243. COQDEP theories/Numbers/Integer/Abstract/ZDivFloor.v
  244. COQDEP theories/Numbers/Integer/Abstract/ZSgnAbs.v
  245. COQDEP theories/Numbers/Integer/Abstract/ZMul.v
  246. COQDEP theories/Numbers/Integer/Abstract/ZMulOrder.v
  247. COQDEP theories/Numbers/Integer/Abstract/ZLt.v
  248. COQDEP theories/Numbers/Integer/Abstract/ZBase.v
  249. COQDEP theories/Numbers/Integer/Abstract/ZAxioms.v
  250. COQDEP theories/Numbers/Integer/Abstract/ZAdd.v
  251. COQDEP theories/Numbers/Integer/Abstract/ZAddOrder.v
  252. COQDEP theories/Numbers/Cyclic/ZModulo/ZModulo.v
  253. COQDEP theories/Numbers/Cyclic/Int31/Ring31.v
  254. COQDEP theories/Numbers/Cyclic/Int31/Cyclic31.v
  255. COQDEP theories/Numbers/Cyclic/Int31/Int31.v
  256. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
  257. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
  258. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
  259. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
  260. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
  261. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
  262. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
  263. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
  264. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
  265. COQDEP theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
  266. COQDEP theories/Numbers/Cyclic/Abstract/NZCyclic.v
  267. COQDEP theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
  268. COQDEP theories/Numbers/BigNumPrelude.v
  269. COQDEP theories/Numbers/BinNums.v
  270. COQDEP theories/QArith/Qminmax.v
  271. COQDEP theories/QArith/QOrderedType.v
  272. COQDEP theories/QArith/Qround.v
  273. COQDEP theories/QArith/Qring.v
  274. COQDEP theories/QArith/Qreduction.v
  275. COQDEP theories/QArith/Qreals.v
  276. COQDEP theories/QArith/Qpower.v
  277. COQDEP theories/QArith/Qfield.v
  278. COQDEP theories/QArith/Qcanon.v
  279. COQDEP theories/QArith/QArith.v
  280. COQDEP theories/QArith/QArith_base.v
  281. COQDEP theories/QArith/Qabs.v
  282. COQDEP theories/Sorting/Mergesort.v
  283. COQDEP theories/Sorting/Sorting.v
  284. COQDEP theories/Sorting/Sorted.v
  285. COQDEP theories/Sorting/PermutEq.v
  286. COQDEP theories/Sorting/PermutSetoid.v
  287. COQDEP theories/Sorting/Permutation.v
  288. COQDEP theories/Sorting/Heap.v
  289. COQDEP theories/Reals/Rminmax.v
  290. COQDEP theories/Reals/ROrderedType.v
  291. COQDEP theories/Reals/Sqrt_reg.v
  292. COQDEP theories/Reals/SplitRmult.v
  293. COQDEP theories/Reals/SplitAbsolu.v
  294. COQDEP theories/Reals/SeqSeries.v
  295. COQDEP theories/Reals/SeqProp.v
  296. COQDEP theories/Reals/Rtrigo.v
  297. COQDEP theories/Reals/Rtrigo1.v
  298. COQDEP theories/Reals/Rtrigo_reg.v
  299. COQDEP theories/Reals/Rtrigo_fun.v
  300. COQDEP theories/Reals/Rtrigo_def.v
  301. COQDEP theories/Reals/Rtrigo_calc.v
  302. COQDEP theories/Reals/Rtrigo_alt.v
  303. COQDEP theories/Reals/Rtopology.v
  304. COQDEP theories/Reals/R_sqr.v
  305. COQDEP theories/Reals/R_sqrt.v
  306. COQDEP theories/Reals/Rsqrt_def.v
  307. COQDEP theories/Reals/Rsigma.v
  308. COQDEP theories/Reals/Rseries.v
  309. COQDEP theories/Reals/Rprod.v
  310. COQDEP theories/Reals/Rpower.v
  311. COQDEP theories/Reals/Rpow_def.v
  312. COQDEP theories/Reals/Rlogic.v
  313. COQDEP theories/Reals/RList.v
  314. COQDEP theories/Reals/Rlimit.v
  315. COQDEP theories/Reals/RIneq.v
  316. COQDEP theories/Reals/R_Ifp.v
  317. COQDEP theories/Reals/RiemannInt.v
  318. COQDEP theories/Reals/RiemannInt_SF.v
  319. COQDEP theories/Reals/Rgeom.v
  320. COQDEP theories/Reals/Rfunctions.v
  321. COQDEP theories/Reals/Reals.v
  322. COQDEP theories/Reals/Rderiv.v
  323. COQDEP theories/Reals/Rdefinitions.v
  324. COQDEP theories/Reals/Rcomplete.v
  325. COQDEP theories/Reals/Rbasic_fun.v
  326. COQDEP theories/Reals/Rbase.v
  327. COQDEP theories/Reals/Raxioms.v
  328. COQDEP theories/Reals/Ratan.v
  329. COQDEP theories/Reals/Ranalysis_reg.v
  330. COQDEP theories/Reals/Ranalysis.v
  331. COQDEP theories/Reals/Ranalysis5.v
  332. COQDEP theories/Reals/Ranalysis4.v
  333. COQDEP theories/Reals/Ranalysis3.v
  334. COQDEP theories/Reals/Ranalysis2.v
  335. COQDEP theories/Reals/Ranalysis1.v
  336. COQDEP theories/Reals/PSeries_reg.v
  337. COQDEP theories/Reals/PartSum.v
  338. COQDEP theories/Reals/NewtonInt.v
  339. COQDEP theories/Reals/MVT.v
  340. COQDEP theories/Reals/Machin.v
  341. COQDEP theories/Reals/LegacyRfield.v
  342. COQDEP theories/Reals/Integration.v
  343. COQDEP theories/Reals/Exp_prop.v
  344. COQDEP theories/Reals/DiscrR.v
  345. COQDEP theories/Reals/Cos_rel.v
  346. COQDEP theories/Reals/Cos_plus.v
  347. COQDEP theories/Reals/Cauchy_prod.v
  348. COQDEP theories/Reals/Binomial.v
  349. COQDEP theories/Reals/ArithProp.v
  350. COQDEP theories/Reals/AltSeries.v
  351. COQDEP theories/Reals/Alembert.v
  352. COQDEP theories/Wellfounded/Well_Ordering.v
  353. COQDEP theories/Wellfounded/Wellfounded.v
  354. COQDEP theories/Wellfounded/Union.v
  355. COQDEP theories/Wellfounded/Transitive_Closure.v
  356. COQDEP theories/Wellfounded/Lexicographic_Product.v
  357. COQDEP theories/Wellfounded/Lexicographic_Exponentiation.v
  358. COQDEP theories/Wellfounded/Inverse_Image.v
  359. COQDEP theories/Wellfounded/Inclusion.v
  360. COQDEP theories/Wellfounded/Disjoint_Union.v
  361. COQDEP theories/Relations/Relations.v
  362. COQDEP theories/Relations/Relation_Operators.v
  363. COQDEP theories/Relations/Relation_Definitions.v
  364. COQDEP theories/Relations/Operators_Properties.v
  365. COQDEP theories/MSets/MSetPositive.v
  366. COQDEP theories/MSets/MSetWeakList.v
  367. COQDEP theories/MSets/MSetToFiniteSet.v
  368. COQDEP theories/MSets/MSets.v
  369. COQDEP theories/MSets/MSetProperties.v
  370. COQDEP theories/MSets/MSetList.v
  371. COQDEP theories/MSets/MSetInterface.v
  372. COQDEP theories/MSets/MSetFacts.v
  373. COQDEP theories/MSets/MSetEqProperties.v
  374. COQDEP theories/MSets/MSetDecide.v
  375. COQDEP theories/MSets/MSetRBT.v
  376. COQDEP theories/MSets/MSetAVL.v
  377. COQDEP theories/MSets/MSetGenTree.v
  378. COQDEP theories/FSets/FSetWeakList.v
  379. COQDEP theories/FSets/FSetToFiniteSet.v
  380. COQDEP theories/FSets/FSets.v
  381. COQDEP theories/FSets/FSetProperties.v
  382. COQDEP theories/FSets/FSetList.v
  383. COQDEP theories/FSets/FSetInterface.v
  384. COQDEP theories/FSets/FSetFacts.v
  385. COQDEP theories/FSets/FSetEqProperties.v
  386. COQDEP theories/FSets/FSetDecide.v
  387. COQDEP theories/FSets/FSetBridge.v
  388. COQDEP theories/FSets/FSetPositive.v
  389. COQDEP theories/FSets/FSetAVL.v
  390. COQDEP theories/FSets/FSetCompat.v
  391. COQDEP theories/FSets/FMapWeakList.v
  392. COQDEP theories/FSets/FMaps.v
  393. COQDEP theories/FSets/FMapPositive.v
  394. COQDEP theories/FSets/FMapList.v
  395. COQDEP theories/FSets/FMapInterface.v
  396. COQDEP theories/FSets/FMapFullAVL.v
  397. COQDEP theories/FSets/FMapFacts.v
  398. COQDEP theories/FSets/FMapAVL.v
  399. COQDEP theories/Sets/Uniset.v
  400. COQDEP theories/Sets/Relations_3.v
  401. COQDEP theories/Sets/Relations_3_facts.v
  402. COQDEP theories/Sets/Relations_2.v
  403. COQDEP theories/Sets/Relations_2_facts.v
  404. COQDEP theories/Sets/Relations_1.v
  405. COQDEP theories/Sets/Relations_1_facts.v
  406. COQDEP theories/Sets/Powerset.v
  407. COQDEP theories/Sets/Powerset_facts.v
  408. COQDEP theories/Sets/Powerset_Classical_facts.v
  409. COQDEP theories/Sets/Permut.v
  410. COQDEP theories/Sets/Partial_Order.v
  411. COQDEP theories/Sets/Multiset.v
  412. COQDEP theories/Sets/Integers.v
  413. COQDEP theories/Sets/Infinite_sets.v
  414. COQDEP theories/Sets/Image.v
  415. COQDEP theories/Sets/Finite_sets.v
  416. COQDEP theories/Sets/Finite_sets_facts.v
  417. COQDEP theories/Sets/Ensembles.v
  418. COQDEP theories/Sets/Cpo.v
  419. COQDEP theories/Sets/Constructive_sets.v
  420. COQDEP theories/Sets/Classical_sets.v
  421. COQDEP theories/Strings/String.v
  422. COQDEP theories/Strings/Ascii.v
  423. COQDEP theories/Lists/Streams.v
  424. COQDEP theories/Lists/StreamMemo.v
  425. COQDEP theories/Lists/SetoidPermutation.v
  426. COQDEP theories/Lists/SetoidList.v
  427. COQDEP theories/Lists/List.v
  428. COQDEP theories/Lists/ListTactics.v
  429. COQDEP theories/Lists/ListSet.v
  430. COQDEP theories/Setoids/Setoid.v
  431. COQDEP theories/ZArith/Zeuclid.v
  432. COQDEP theories/ZArith/Zwf.v
  433. COQDEP theories/ZArith/Zsqrt_compat.v
  434. COQDEP theories/ZArith/Zpow_facts.v
  435. COQDEP theories/ZArith/Zpower.v
  436. COQDEP theories/ZArith/Zpow_def.v
  437. COQDEP theories/ZArith/Zorder.v
  438. COQDEP theories/ZArith/Zquot.v
  439. COQDEP theories/ZArith/ZOdiv.v
  440. COQDEP theories/ZArith/ZOdiv_def.v
  441. COQDEP theories/ZArith/Znumtheory.v
  442. COQDEP theories/ZArith/Znat.v
  443. COQDEP theories/ZArith/Zmisc.v
  444. COQDEP theories/ZArith/Zmin.v
  445. COQDEP theories/ZArith/Zminmax.v
  446. COQDEP theories/ZArith/Zmax.v
  447. COQDEP theories/ZArith/Zlogarithm.v
  448. COQDEP theories/ZArith/Zhints.v
  449. COQDEP theories/ZArith/Zpow_alt.v
  450. COQDEP theories/ZArith/Zgcd_alt.v
  451. COQDEP theories/ZArith/Zeven.v
  452. COQDEP theories/ZArith/Zdiv.v
  453. COQDEP theories/ZArith/Zcomplements.v
  454. COQDEP theories/ZArith/Zcompare.v
  455. COQDEP theories/ZArith/Zbool.v
  456. COQDEP theories/ZArith/Zdigits.v
  457. COQDEP theories/ZArith/ZArith.v
  458. COQDEP theories/ZArith/ZArith_dec.v
  459. COQDEP theories/ZArith/ZArith_base.v
  460. COQDEP theories/ZArith/Zabs.v
  461. COQDEP theories/ZArith/Wf_Z.v
  462. COQDEP theories/ZArith/Int.v
  463. COQDEP theories/ZArith/BinInt.v
  464. COQDEP theories/ZArith/BinIntDef.v
  465. COQDEP theories/ZArith/auxiliary.v
  466. COQDEP theories/NArith/Ngcd_def.v
  467. COQDEP theories/NArith/Nsqrt_def.v
  468. COQDEP theories/NArith/Ndiv_def.v
  469. COQDEP theories/NArith/Nnat.v
  470. COQDEP theories/NArith/Ndist.v
  471. COQDEP theories/NArith/Ndigits.v
  472. COQDEP theories/NArith/Ndec.v
  473. COQDEP theories/NArith/NArith.v
  474. COQDEP theories/NArith/BinNat.v
  475. COQDEP theories/NArith/BinNatDef.v
  476. COQDEP theories/PArith/PArith.v
  477. COQDEP theories/PArith/POrderedType.v
  478. COQDEP theories/PArith/Pnat.v
  479. COQDEP theories/PArith/BinPos.v
  480. COQDEP theories/PArith/BinPosDef.v
  481. COQDEP theories/Bool/Zerob.v
  482. COQDEP theories/Bool/Sumbool.v
  483. COQDEP theories/Bool/IfProp.v
  484. COQDEP theories/Bool/DecBool.v
  485. COQDEP theories/Bool/Bvector.v
  486. COQDEP theories/Bool/Bool.v
  487. COQDEP theories/Bool/BoolEq.v
  488. COQDEP theories/Arith/Wf_nat.v
  489. COQDEP theories/Arith/Plus.v
  490. COQDEP theories/Arith/Peano_dec.v
  491. COQDEP theories/Arith/Mult.v
  492. COQDEP theories/Arith/Min.v
  493. COQDEP theories/Arith/Minus.v
  494. COQDEP theories/Arith/Max.v
  495. COQDEP theories/Arith/Lt.v
  496. COQDEP theories/Arith/Le.v
  497. COQDEP theories/Arith/Gt.v
  498. COQDEP theories/Arith/Factorial.v
  499. COQDEP theories/Arith/Even.v
  500. COQDEP theories/Arith/Euclid.v
  501. COQDEP theories/Arith/EqNat.v
  502. COQDEP theories/Arith/Div2.v
  503. COQDEP theories/Arith/Compare.v
  504. COQDEP theories/Arith/Compare_dec.v
  505. COQDEP theories/Arith/Bool_nat.v
  506. COQDEP theories/Arith/Between.v
  507. COQDEP theories/Arith/Arith.v
  508. COQDEP theories/Arith/Arith_base.v
  509. COQDEP theories/Logic/SetIsType.v
  510. COQDEP theories/Logic/RelationalChoice.v
  511. COQDEP theories/Logic/ProofIrrelevance.v
  512. COQDEP theories/Logic/ProofIrrelevanceFacts.v
  513. COQDEP theories/Logic/JMeq.v
  514. COQDEP theories/Logic/IndefiniteDescription.v
  515. COQDEP theories/Logic/Hurkens.v
  516. COQDEP theories/Logic/FunctionalExtensionality.v
  517. COQDEP theories/Logic/Eqdep.v
  518. COQDEP theories/Logic/EqdepFacts.v
  519. COQDEP theories/Logic/Eqdep_dec.v
  520. COQDEP theories/Logic/Epsilon.v
  521. COQDEP theories/Logic/Diaconescu.v
  522. COQDEP theories/Logic/Description.v
  523. COQDEP theories/Logic/Decidable.v
  524. COQDEP theories/Logic/ConstructiveEpsilon.v
  525. COQDEP theories/Logic/Classical.v
  526. COQDEP theories/Logic/ClassicalUniqueChoice.v
  527. COQDEP theories/Logic/Classical_Type.v
  528. COQDEP theories/Logic/Classical_Prop.v
  529. COQDEP theories/Logic/Classical_Pred_Type.v
  530. COQDEP theories/Logic/Classical_Pred_Set.v
  531. COQDEP theories/Logic/ClassicalFacts.v
  532. COQDEP theories/Logic/ClassicalEpsilon.v
  533. COQDEP theories/Logic/ClassicalDescription.v
  534. COQDEP theories/Logic/ClassicalChoice.v
  535. COQDEP theories/Logic/ChoiceFacts.v
  536. COQDEP theories/Logic/Berardi.v
  537. COQDEP theories/Init/Wf.v
  538. COQDEP theories/Init/Tactics.v
  539. COQDEP theories/Init/Specif.v
  540. COQDEP theories/Init/Prelude.v
  541. COQDEP theories/Init/Peano.v
  542. COQDEP theories/Init/Notations.v
  543. COQDEP theories/Init/Logic.v
  544. COQDEP theories/Init/Logic_Type.v
  545. COQDEP theories/Init/Datatypes.v
  546. OCAMLLEX ide/utf8_convert.mll
  547. 15 states, 827 transitions, table size 3398 bytes
  548. OCAMLLEX ide/config_lexer.mll
  549. 30 states, 1657 transitions, table size 6808 bytes
  550. 6096 additional bytes used for bindings
  551. OCAMLLEX ide/coq_lex.mll
  552. ocamllex warning:
  553. File "ide/coq_lex.mll", line 112, character 66: unescaped newline in string.
  554. 454 states, 31913 transitions, table size 130376 bytes
  555. OCAMLLEX tools/coqwc.mll
  556. 230 states, 833 transitions, table size 4712 bytes
  557. OCAMLLEX tools/gallina_lexer.mll
  558. 190 states, 498 transitions, table size 3132 bytes
  559. OCAMLLEX tools/coqdoc/cpretty.mll
  560. 2472 states, 7945 transitions, table size 46612 bytes
  561. OCAMLLEX lib/xml_lexer.mll
  562. 78 states, 800 transitions, table size 3668 bytes
  563. ECHO... > scripts/tolink.ml
  564. sed -n -e '/^enum/p' -e 's/,//g' -e '/^ /p' kernel/byterun/coq_instruct.h | \
  565. awk -f kernel/make-opcodes > "kernel/copcodes.ml" || (RV=$?; rm -f "kernel/copcodes.ml"; exit ${RV})
  566. sed -n -e '/^ /s/ \([A-Z]\)/ \&\&coq_lbl_\1/gp' \
  567. -e '/^}/q' kernel/byterun/coq_instruct.h > "kernel/byterun/coq_jumptbl.h" || (RV=$?; rm -f "kernel/byterun/coq_jumptbl.h"; exit ${RV})
  568. ECHO... > plugins/omega/omega_plugin_mod.ml
  569. ECHO... > plugins/rtauto/rtauto_plugin_mod.ml
  570. ECHO... > plugins/fourier/fourier_plugin_mod.ml
  571. ECHO... > plugins/nsatz/nsatz_plugin_mod.ml
  572. ECHO... > plugins/funind/recdef_plugin_mod.ml
  573. ECHO... > plugins/micromega/micromega_plugin_mod.ml
  574. ECHO... > plugins/xml/xml_plugin_mod.ml
  575. ECHO... > plugins/subtac/subtac_plugin_mod.ml
  576. ECHO... > plugins/quote/quote_plugin_mod.ml
  577. ECHO... > plugins/setoid_ring/newring_plugin_mod.ml
  578. ECHO... > plugins/syntax/r_syntax_plugin_mod.ml
  579. ECHO... > plugins/syntax/ascii_syntax_plugin_mod.ml
  580. ECHO... > plugins/syntax/string_syntax_plugin_mod.ml
  581. ECHO... > plugins/syntax/nat_syntax_plugin_mod.ml
  582. ECHO... > plugins/syntax/numbers_syntax_plugin_mod.ml
  583. ECHO... > plugins/syntax/z_syntax_plugin_mod.ml
  584. ECHO... > plugins/firstorder/ground_plugin_mod.ml
  585. ECHO... > plugins/field/field_plugin_mod.ml
  586. ECHO... > plugins/extraction/extraction_plugin_mod.ml
  587. ECHO... > plugins/cc/cc_plugin_mod.ml
  588. ECHO... > plugins/romega/romega_plugin_mod.ml
  589. ECHO... > plugins/decl_mode/decl_mode_plugin_mod.ml
  590. ECHO... > plugins/ring/ring_plugin_mod.ml
  591. COQDEP parsing/grammar.mllib
  592. COQDEP parsing/parsing.mllib
  593. COQDEP parsing/highparsing.mllib
  594. COQDEP lib/lib.mllib
  595. COQDEP tactics/tactics.mllib
  596. COQDEP tactics/hightactics.mllib
  597. COQDEP proofs/proofs.mllib
  598. COQDEP tools/win32hack.mllib
  599. COQDEP toplevel/toplevel.mllib
  600. COQDEP checker/check.mllib
  601. COQDEP pretyping/pretyping.mllib
  602. COQDEP interp/interp.mllib
  603. COQDEP kernel/kernel.mllib
  604. COQDEP ide/ide.mllib
  605. COQDEP library/library.mllib
  606. COQDEP dev/printers.mllib
  607. COQDEP plugins/ring/ring_plugin.mllib
  608. COQDEP plugins/decl_mode/decl_mode_plugin.mllib
  609. COQDEP plugins/romega/romega_plugin.mllib
  610. COQDEP plugins/cc/cc_plugin.mllib
  611. COQDEP plugins/extraction/extraction_plugin.mllib
  612. COQDEP plugins/field/field_plugin.mllib
  613. COQDEP plugins/firstorder/ground_plugin.mllib
  614. COQDEP plugins/syntax/z_syntax_plugin.mllib
  615. COQDEP plugins/syntax/numbers_syntax_plugin.mllib
  616. COQDEP plugins/syntax/nat_syntax_plugin.mllib
  617. COQDEP plugins/syntax/string_syntax_plugin.mllib
  618. COQDEP plugins/syntax/ascii_syntax_plugin.mllib
  619. COQDEP plugins/syntax/r_syntax_plugin.mllib
  620. COQDEP plugins/setoid_ring/newring_plugin.mllib
  621. COQDEP plugins/quote/quote_plugin.mllib
  622. COQDEP plugins/subtac/subtac_plugin.mllib
  623. COQDEP plugins/xml/xml_plugin.mllib
  624. COQDEP plugins/micromega/micromega_plugin.mllib
  625. COQDEP plugins/funind/recdef_plugin.mllib
  626. COQDEP plugins/nsatz/nsatz_plugin.mllib
  627. COQDEP plugins/fourier/fourier_plugin.mllib
  628. COQDEP plugins/rtauto/rtauto_plugin.mllib
  629. COQDEP plugins/omega/omega_plugin.mllib
  630. CCDEP kernel/byterun/coq_memory.c
  631. CCDEP kernel/byterun/coq_values.c
  632. CCDEP kernel/byterun/coq_fix_code.c
  633. CCDEP kernel/byterun/coq_interp.c
  634. CCDEP ide/ide_win32_stubs.c
  635. OCAMLDEP toplevel/whelp.mli
  636. OCAMLDEP toplevel/vernacinterp.mli
  637. OCAMLDEP toplevel/vernacentries.mli
  638. OCAMLDEP toplevel/vernac.mli
  639. OCAMLDEP toplevel/usage.mli
  640. OCAMLDEP toplevel/toplevel.mli
  641. OCAMLDEP toplevel/search.mli
  642. OCAMLDEP toplevel/record.mli
  643. OCAMLDEP toplevel/mltop.mli
  644. OCAMLDEP toplevel/metasyntax.mli
  645. OCAMLDEP toplevel/libtypes.mli
  646. OCAMLDEP toplevel/lemmas.mli
  647. OCAMLDEP toplevel/interface.mli
  648. OCAMLDEP toplevel/indschemes.mli
  649. OCAMLDEP toplevel/ind_tables.mli
  650. OCAMLDEP toplevel/ide_slave.mli
  651. OCAMLDEP toplevel/ide_intf.mli
  652. OCAMLDEP toplevel/himsg.mli
  653. OCAMLDEP toplevel/discharge.mli
  654. OCAMLDEP toplevel/coqtop.mli
  655. OCAMLDEP toplevel/coqinit.mli
  656. OCAMLDEP toplevel/command.mli
  657. OCAMLDEP toplevel/classes.mli
  658. OCAMLDEP toplevel/class.mli
  659. OCAMLDEP toplevel/cerrors.mli
  660. OCAMLDEP toplevel/backtrack.mli
  661. OCAMLDEP toplevel/autoinstance.mli
  662. OCAMLDEP toplevel/auto_ind_decl.mli
  663. OCAMLDEP tools/coqdoc/tokens.mli
  664. OCAMLDEP tools/coqdoc/output.mli
  665. OCAMLDEP tools/coqdoc/index.mli
  666. OCAMLDEP tools/coqdoc/cpretty.mli
  667. OCAMLDEP tools/coqdoc/alpha.mli
  668. OCAMLDEP tools/coqdep_lexer.mli
  669. OCAMLDEP tools/coqdep_common.mli
  670. OCAMLDEP tactics/termdn.mli
  671. OCAMLDEP tactics/tactics.mli
  672. OCAMLDEP tactics/tacticals.mli
  673. OCAMLDEP tactics/tactic_option.mli
  674. OCAMLDEP tactics/tacinterp.mli
  675. OCAMLDEP tactics/refine.mli
  676. OCAMLDEP tactics/nbtermdn.mli
  677. OCAMLDEP tactics/leminv.mli
  678. OCAMLDEP tactics/inv.mli
  679. OCAMLDEP tactics/hipattern.mli
  680. OCAMLDEP tactics/hiddentac.mli
  681. OCAMLDEP tactics/extratactics.mli
  682. OCAMLDEP tactics/extraargs.mli
  683. OCAMLDEP tactics/evar_tactics.mli
  684. OCAMLDEP tactics/equality.mli
  685. OCAMLDEP tactics/eqschemes.mli
  686. OCAMLDEP tactics/elimschemes.mli
  687. OCAMLDEP tactics/elim.mli
  688. OCAMLDEP tactics/eauto.mli
  689. OCAMLDEP tactics/dn.mli
  690. OCAMLDEP tactics/contradiction.mli
  691. OCAMLDEP tactics/btermdn.mli
  692. OCAMLDEP tactics/autorewrite.mli
  693. OCAMLDEP tactics/auto.mli
  694. OCAMLDEP proofs/tactic_debug.mli
  695. OCAMLDEP proofs/tacmach.mli
  696. OCAMLDEP proofs/refiner.mli
  697. OCAMLDEP proofs/redexpr.mli
  698. OCAMLDEP proofs/proofview.mli
  699. OCAMLDEP proofs/proof_type.mli
  700. OCAMLDEP proofs/proof_global.mli
  701. OCAMLDEP proofs/proof.mli
  702. OCAMLDEP proofs/pfedit.mli
  703. OCAMLDEP proofs/logic.mli
  704. OCAMLDEP proofs/goal.mli
  705. OCAMLDEP proofs/evar_refiner.mli
  706. OCAMLDEP proofs/clenvtac.mli
  707. OCAMLDEP proofs/clenv.mli
  708. OCAMLDEP pretyping/vnorm.mli
  709. OCAMLDEP pretyping/unification.mli
  710. OCAMLDEP pretyping/typing.mli
  711. OCAMLDEP pretyping/typeclasses_errors.mli
  712. OCAMLDEP pretyping/typeclasses.mli
  713. OCAMLDEP pretyping/termops.mli
  714. OCAMLDEP pretyping/term_dnet.mli
  715. OCAMLDEP pretyping/tacred.mli
  716. OCAMLDEP pretyping/retyping.mli
  717. OCAMLDEP pretyping/reductionops.mli
  718. OCAMLDEP pretyping/recordops.mli
  719. OCAMLDEP pretyping/pretyping.mli
  720. OCAMLDEP pretyping/pretype_errors.mli
  721. OCAMLDEP pretyping/pattern.mli
  722. OCAMLDEP pretyping/namegen.mli
  723. OCAMLDEP pretyping/matching.mli
  724. OCAMLDEP pretyping/inductiveops.mli
  725. OCAMLDEP pretyping/indrec.mli
  726. OCAMLDEP pretyping/glob_term.mli
  727. OCAMLDEP pretyping/evd.mli
  728. OCAMLDEP pretyping/evarutil.mli
  729. OCAMLDEP pretyping/evarconv.mli
  730. OCAMLDEP pretyping/detyping.mli
  731. OCAMLDEP pretyping/coercion.mli
  732. OCAMLDEP pretyping/classops.mli
  733. OCAMLDEP pretyping/cbv.mli
  734. OCAMLDEP pretyping/cases.mli
  735. OCAMLDEP pretyping/arguments_renaming.mli
  736. OCAMLDEP plugins/xml/xmlcommand.mli
  737. OCAMLDEP plugins/xml/xml.mli
  738. OCAMLDEP plugins/xml/unshare.mli
  739. OCAMLDEP plugins/xml/doubleTypeInference.mli
  740. OCAMLDEP plugins/subtac/subtac_utils.mli
  741. OCAMLDEP plugins/subtac/subtac_pretyping.mli
  742. OCAMLDEP plugins/subtac/subtac_obligations.mli
  743. OCAMLDEP plugins/subtac/subtac_errors.mli
  744. OCAMLDEP plugins/subtac/subtac_command.mli
  745. OCAMLDEP plugins/subtac/subtac_coercion.mli
  746. OCAMLDEP plugins/subtac/subtac_classes.mli
  747. OCAMLDEP plugins/subtac/subtac_cases.mli
  748. OCAMLDEP plugins/subtac/subtac.mli
  749. OCAMLDEP plugins/subtac/eterm.mli
  750. OCAMLDEP plugins/rtauto/refl_tauto.mli
  751. OCAMLDEP plugins/rtauto/proof_search.mli
  752. OCAMLDEP plugins/romega/const_omega.mli
  753. OCAMLDEP plugins/nsatz/utile.mli
  754. OCAMLDEP plugins/nsatz/polynom.mli
  755. OCAMLDEP plugins/micromega/sos.mli
  756. OCAMLDEP plugins/micromega/micromega.mli
  757. OCAMLDEP plugins/funind/indfun_common.mli
  758. OCAMLDEP plugins/funind/indfun.mli
  759. OCAMLDEP plugins/funind/glob_termops.mli
  760. OCAMLDEP plugins/funind/glob_term_to_relation.mli
  761. OCAMLDEP plugins/funind/functional_principles_types.mli
  762. OCAMLDEP plugins/funind/functional_principles_proofs.mli
  763. OCAMLDEP plugins/firstorder/unify.mli
  764. OCAMLDEP plugins/firstorder/sequent.mli
  765. OCAMLDEP plugins/firstorder/rules.mli
  766. OCAMLDEP plugins/firstorder/instances.mli
  767. OCAMLDEP plugins/firstorder/ground.mli
  768. OCAMLDEP plugins/firstorder/formula.mli
  769. OCAMLDEP plugins/extraction/table.mli
  770. OCAMLDEP plugins/extraction/scheme.mli
  771. OCAMLDEP plugins/extraction/ocaml.mli
  772. OCAMLDEP plugins/extraction/modutil.mli
  773. OCAMLDEP plugins/extraction/mlutil.mli
  774. OCAMLDEP plugins/extraction/miniml.mli
  775. OCAMLDEP plugins/extraction/haskell.mli
  776. OCAMLDEP plugins/extraction/extraction.mli
  777. OCAMLDEP plugins/extraction/extract_env.mli
  778. OCAMLDEP plugins/extraction/common.mli
  779. OCAMLDEP plugins/decl_mode/ppdecl_proof.mli
  780. OCAMLDEP plugins/decl_mode/decl_proof_instr.mli
  781. OCAMLDEP plugins/decl_mode/decl_mode.mli
  782. OCAMLDEP plugins/decl_mode/decl_interp.mli
  783. OCAMLDEP plugins/decl_mode/decl_expr.mli
  784. OCAMLDEP plugins/cc/cctac.mli
  785. OCAMLDEP plugins/cc/ccproof.mli
  786. OCAMLDEP plugins/cc/ccalgo.mli
  787. OCAMLDEP parsing/tok.mli
  788. OCAMLDEP parsing/tactic_printer.mli
  789. OCAMLDEP parsing/q_util.mli
  790. OCAMLDEP parsing/printmod.mli
  791. OCAMLDEP parsing/printer.mli
  792. OCAMLDEP parsing/prettyp.mli
  793. OCAMLDEP parsing/ppvernac.mli
  794. OCAMLDEP parsing/pptactic.mli
  795. OCAMLDEP parsing/ppconstr.mli
  796. OCAMLDEP parsing/pcoq.mli
  797. OCAMLDEP parsing/lexer.mli
  798. OCAMLDEP parsing/extrawit.mli
  799. OCAMLDEP parsing/extend.mli
  800. OCAMLDEP parsing/egrammar.mli
  801. OCAMLDEP library/summary.mli
  802. OCAMLDEP library/states.mli
  803. OCAMLDEP library/nametab.mli
  804. OCAMLDEP library/nameops.mli
  805. OCAMLDEP library/library.mli
  806. OCAMLDEP library/libobject.mli
  807. OCAMLDEP library/libnames.mli
  808. OCAMLDEP library/lib.mli
  809. OCAMLDEP library/impargs.mli
  810. OCAMLDEP library/heads.mli
  811. OCAMLDEP library/goptionstyp.mli
  812. OCAMLDEP library/goptions.mli
  813. OCAMLDEP library/global.mli
  814. OCAMLDEP library/dischargedhypsmap.mli
  815. OCAMLDEP library/decls.mli
  816. OCAMLDEP library/declaremods.mli
  817. OCAMLDEP library/declare.mli
  818. OCAMLDEP library/decl_kinds.mli
  819. OCAMLDEP library/assumptions.mli
  820. OCAMLDEP lib/xml_utils.mli
  821. OCAMLDEP lib/xml_parser.mli
  822. OCAMLDEP lib/xml_lexer.mli
  823. OCAMLDEP lib/util.mli
  824. OCAMLDEP lib/unionfind.mli
  825. OCAMLDEP lib/tries.mli
  826. OCAMLDEP lib/system.mli
  827. OCAMLDEP lib/store.mli
  828. OCAMLDEP lib/segmenttree.mli
  829. OCAMLDEP lib/rtree.mli
  830. OCAMLDEP lib/profile.mli
  831. OCAMLDEP lib/predicate.mli
  832. OCAMLDEP lib/pp_control.mli
  833. OCAMLDEP lib/pp.mli
  834. OCAMLDEP lib/option.mli
  835. OCAMLDEP lib/heap.mli
  836. OCAMLDEP lib/hashtbl_alt.mli
  837. OCAMLDEP lib/hashcons.mli
  838. OCAMLDEP lib/gmapl.mli
  839. OCAMLDEP lib/gmap.mli
  840. OCAMLDEP lib/fset.mli
  841. OCAMLDEP lib/fmap.mli
  842. OCAMLDEP lib/flags.mli
  843. OCAMLDEP lib/explore.mli
  844. OCAMLDEP lib/errors.mli
  845. OCAMLDEP lib/envars.mli
  846. OCAMLDEP lib/dyn.mli
  847. OCAMLDEP lib/dnet.mli
  848. OCAMLDEP lib/bigint.mli
  849. OCAMLDEP kernel/vm.mli
  850. OCAMLDEP kernel/vconv.mli
  851. OCAMLDEP kernel/univ.mli
  852. OCAMLDEP kernel/typeops.mli
  853. OCAMLDEP kernel/type_errors.mli
  854. OCAMLDEP kernel/term_typing.mli
  855. OCAMLDEP kernel/term.mli
  856. OCAMLDEP kernel/subtyping.mli
  857. OCAMLDEP kernel/sign.mli
  858. OCAMLDEP kernel/safe_typing.mli
  859. OCAMLDEP kernel/retroknowledge.mli
  860. OCAMLDEP kernel/reduction.mli
  861. OCAMLDEP kernel/pre_env.mli
  862. OCAMLDEP kernel/names.mli
  863. OCAMLDEP kernel/modops.mli
  864. OCAMLDEP kernel/mod_typing.mli
  865. OCAMLDEP kernel/mod_subst.mli
  866. OCAMLDEP kernel/inductive.mli
  867. OCAMLDEP kernel/indtypes.mli
  868. OCAMLDEP kernel/esubst.mli
  869. OCAMLDEP kernel/environ.mli
  870. OCAMLDEP kernel/entries.mli
  871. OCAMLDEP kernel/declarations.mli
  872. OCAMLDEP kernel/csymtable.mli
  873. OCAMLDEP kernel/cooking.mli
  874. OCAMLDEP kernel/conv_oracle.mli
  875. OCAMLDEP kernel/closure.mli
  876. OCAMLDEP kernel/cemitcodes.mli
  877. OCAMLDEP kernel/cbytegen.mli
  878. OCAMLDEP kernel/cbytecodes.mli
  879. OCAMLDEP interp/topconstr.mli
  880. OCAMLDEP interp/syntax_def.mli
  881. OCAMLDEP interp/smartlocate.mli
  882. OCAMLDEP interp/reserve.mli
  883. OCAMLDEP interp/ppextend.mli
  884. OCAMLDEP interp/notation.mli
  885. OCAMLDEP interp/modintern.mli
  886. OCAMLDEP interp/implicit_quantifiers.mli
  887. OCAMLDEP interp/genarg.mli
  888. OCAMLDEP interp/dumpglob.mli
  889. OCAMLDEP interp/coqlib.mli
  890. OCAMLDEP interp/constrintern.mli
  891. OCAMLDEP interp/constrextern.mli
  892. OCAMLDEP ide/utils/okey.mli
  893. OCAMLDEP ide/utils/configwin.mli
  894. OCAMLDEP ide/utils/config_file.mli
  895. OCAMLDEP ide/undo_lablgtk_lt26.mli
  896. OCAMLDEP ide/undo_lablgtk_ge26.mli
  897. OCAMLDEP ide/undo_lablgtk_ge212.mli
  898. OCAMLDEP ide/undo.mli
  899. OCAMLDEP ide/tags.mli
  900. OCAMLDEP ide/preferences.mli
  901. OCAMLDEP ide/minilib.mli
  902. OCAMLDEP ide/ideutils.mli
  903. OCAMLDEP ide/coqide.mli
  904. OCAMLDEP ide/coq.mli
  905. OCAMLDEP ide/command_windows.mli
  906. OCAMLDEP config/coq_config.mli
  907. OCAMLDEP checker/typeops.mli
  908. OCAMLDEP checker/type_errors.mli
  909. OCAMLDEP checker/term.mli
  910. OCAMLDEP checker/subtyping.mli
  911. OCAMLDEP checker/safe_typing.mli
  912. OCAMLDEP checker/reduction.mli
  913. OCAMLDEP checker/modops.mli
  914. OCAMLDEP checker/mod_checking.mli
  915. OCAMLDEP checker/inductive.mli
  916. OCAMLDEP checker/indtypes.mli
  917. OCAMLDEP checker/environ.mli
  918. OCAMLDEP checker/declarations.mli
  919. OCAMLDEP checker/closure.mli
  920. OCAMLDEP checker/check_stat.mli
  921. OCAMLDEP plugins/ring/ring_plugin_mod.ml
  922. OCAMLDEP plugins/decl_mode/decl_mode_plugin_mod.ml
  923. OCAMLDEP plugins/romega/romega_plugin_mod.ml
  924. OCAMLDEP plugins/cc/cc_plugin_mod.ml
  925. OCAMLDEP plugins/extraction/extraction_plugin_mod.ml
  926. OCAMLDEP plugins/field/field_plugin_mod.ml
  927. OCAMLDEP plugins/firstorder/ground_plugin_mod.ml
  928. OCAMLDEP plugins/syntax/z_syntax_plugin_mod.ml
  929. OCAMLDEP plugins/syntax/numbers_syntax_plugin_mod.ml
  930. OCAMLDEP plugins/syntax/nat_syntax_plugin_mod.ml
  931. OCAMLDEP plugins/syntax/string_syntax_plugin_mod.ml
  932. OCAMLDEP plugins/syntax/ascii_syntax_plugin_mod.ml
  933. OCAMLDEP plugins/syntax/r_syntax_plugin_mod.ml
  934. OCAMLDEP plugins/setoid_ring/newring_plugin_mod.ml
  935. OCAMLDEP plugins/quote/quote_plugin_mod.ml
  936. OCAMLDEP plugins/subtac/subtac_plugin_mod.ml
  937. OCAMLDEP plugins/xml/xml_plugin_mod.ml
  938. OCAMLDEP plugins/micromega/micromega_plugin_mod.ml
  939. OCAMLDEP plugins/funind/recdef_plugin_mod.ml
  940. OCAMLDEP plugins/nsatz/nsatz_plugin_mod.ml
  941. OCAMLDEP plugins/fourier/fourier_plugin_mod.ml
  942. OCAMLDEP plugins/rtauto/rtauto_plugin_mod.ml
  943. OCAMLDEP plugins/omega/omega_plugin_mod.ml
  944. "ocamlc.opt" -rectypes -c -I "+camlp4" -pp 'camlp4orf -impl' -impl tools/compat5.mlp
  945. File "tools/compat5.mlp", line 1:
  946. Error: The files /usr/lib/ocaml/pervasives.cmi
  947. and /usr/lib/ocaml/camlp4/Camlp4.cmi make inconsistent assumptions
  948. over interface Pervasives
  949. Makefile.build:563: recipe for target 'tools/compat5.cmo' failed
  950. make[1]: *** [tools/compat5.cmo] Error 2
  951. make[1]: Leaving directory '/home/thorsten/tmp.aur/coq/src/coq-8.4pl5'
  952. Makefile:139: recipe for target 'world' failed
  953. make: *** [world] Error 2
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!