Advertisement
Guest User

Coq build failure on archlinux with ocaml 4.02.1

a guest
Dec 22nd, 2014
376
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 37.44 KB | None | 0 0
  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