Permalink
Browse files

Merge with trunk, again

  • Loading branch information...
andrejbauer committed Oct 12, 2012
2 parents 9379605 + 3b5a042 commit 90867e61762826ac7fff185e8bdc9ca6bc6f4250
Showing with 1,715 additions and 3,471 deletions.
  1. +1 −4 .gitignore
  2. +46 −37 Makefile.build
  3. +2 −2 Makefile.common
  4. +14 −17 _tags
  5. +1 −1 build
  6. +1 −1 checker/check.mllib
  7. +0 −5 checker/check_stat.ml
  8. +1 −4 checker/checker.ml
  9. +0 −1 checker/closure.ml
  10. +1 −2 checker/declarations.ml
  11. +0 −1 checker/mod_checking.ml
  12. +0 −2 checker/modops.ml
  13. +0 −1 checker/reduction.ml
  14. +0 −3 checker/subtyping.ml
  15. +1 −2 checker/term.ml
  16. +1 −1 checker/typeops.ml
  17. +1 −1 checker/validate.ml
  18. +0 −1 config/coq_config.mli
  19. +40 −42 configure
  20. +0 −9 dev/doc/debugging.txt
  21. +0 −31 dev/doc/patch.ocaml-3.10.drop.rectypes
  22. +51 −0 dev/dynlink.ml
  23. +3 −3 dev/printers.mllib
  24. +0 −9 dev/top_printers.ml
  25. +16 −23 grammar/argextend.ml4
  26. +2 −1 grammar/grammar.mllib
  27. +4 −10 grammar/q_constr.ml4
  28. +41 −19 grammar/q_coqast.ml4
  29. +6 −11 grammar/q_util.ml4
  30. +20 −15 grammar/tacextend.ml4
  31. +5 −6 grammar/vernacextend.ml4
  32. +1 −36 interp/constrintern.ml
  33. +0 −55 interp/modintern.ml
  34. +0 −2 interp/notation.ml
  35. +0 −1 interp/smartlocate.ml
  36. +1 −13 interp/topconstr.ml
  37. +0 −2 intf/constrexpr.mli
  38. +10 −1 intf/extend.mli
  39. +0 −4 intf/glob_term.mli
  40. +13 −2 intf/misctypes.mli
  41. +0 −1 intf/notation_term.mli
  42. +141 −153 intf/tacexpr.mli
  43. +1 −1 intf/vernacexpr.mli
  44. +2 −11 kernel/byterun/coq_fix_code.c
  45. +0 −1 kernel/byterun/coq_fix_code.h
  46. +1 −1 kernel/byterun/coq_instruct.h
  47. +0 −20 kernel/byterun/coq_interp.c
  48. +0 −34 kernel/byterun/coq_memory.c
  49. +0 −3 kernel/byterun/coq_memory.h
  50. +2 −39 kernel/csymtable.ml
  51. +0 −2 kernel/mod_subst.ml
  52. +0 −3 kernel/modops.ml
  53. +25 −20 kernel/names.ml
  54. +0 −2 kernel/pre_env.ml
  55. +10 −8 kernel/term.ml
  56. +8 −10 kernel/univ.ml
  57. +0 −8 kernel/vm.ml
  58. +0 −6 kernel/vm.mli
  59. +0 −12 lib/cList.ml
  60. +6 −8 lib/dnet.ml
  61. +2 −4 lib/dnet.mli
  62. +0 −1 lib/dyn.ml
  63. +0 −1 lib/gmapl.ml
  64. +20 −25 lib/hashcons.ml
  65. +58 −14 lib/hashcons.mli
  66. +48 −44 lib/{hashtbl_alt.ml → hashset.ml}
  67. +45 −0 lib/hashset.mli
  68. +0 −41 lib/hashtbl_alt.mli
  69. +1 −2 lib/lib.mllib
  70. +51 −13 lib/loc.ml
  71. +17 −4 lib/loc.mli
  72. +0 −5 lib/serialize.ml
  73. +0 −10 lib/store.ml
  74. +9 −8 lib/system.ml
  75. +0 −5 lib/util.ml
  76. +0 −1 lib/xml_parser.ml
  77. +0 −1 library/declaremods.ml
  78. +0 −1 library/dischargedhypsmap.ml
  79. +0 −1 library/global.ml
  80. +0 −1 library/globnames.ml
  81. +0 −2 library/goptions.ml
  82. +0 −2 library/impargs.ml
  83. +2 −11 library/lib.ml
  84. +0 −1 library/libobject.ml
  85. +0 −2 library/library.ml
  86. +35 −29 library/nametab.ml
  87. +4 −26 myocamlbuild.ml
  88. +93 −30 {lib → parsing}/compat.ml4
  89. +71 −44 parsing/egramcoq.ml
  90. +14 −5 parsing/egramcoq.mli
  91. +1 −1 parsing/egramml.ml
  92. +3 −5 parsing/extrawit.ml
  93. +65 −67 parsing/g_constr.ml4
  94. +14 −14 parsing/g_ltac.ml4
  95. +0 −11 parsing/g_obligations.ml4
  96. +17 −16 parsing/g_prim.ml4
  97. +2 −1 parsing/g_proofs.ml4
  98. +25 −25 parsing/g_tactic.ml4
  99. +21 −23 parsing/g_vernac.ml4
  100. +5 −6 parsing/g_xml.ml4
  101. +5 −6 parsing/lexer.ml4
  102. +1 −1 parsing/lexer.mli
  103. +1 −0 parsing/parsing.mllib
  104. +34 −39 parsing/pcoq.ml4
  105. +5 −5 parsing/pcoq.mli
  106. +1 −3 plugins/cc/ccalgo.ml
  107. +0 −1 plugins/cc/ccproof.ml
  108. +0 −2 plugins/cc/g_congruence.ml4
  109. +0 −1 plugins/decl_mode/decl_mode.ml
  110. +0 −17 plugins/decl_mode/decl_proof_instr.ml
  111. +3 −5 plugins/decl_mode/g_decl_mode.ml4
  112. +0 −1 plugins/decl_mode/ppdecl_proof.ml
  113. +3 −7 plugins/extraction/extract_env.ml
  114. +0 −2 plugins/extraction/g_extraction.ml4
  115. +0 −5 plugins/extraction/haskell.ml
  116. +0 −15 plugins/extraction/mlutil.ml
  117. +0 −2 plugins/extraction/modutil.ml
  118. +1 −4 plugins/firstorder/g_ground.ml4
  119. +0 −4 plugins/firstorder/sequent.ml
  120. +0 −2 plugins/fourier/fourierR.ml
  121. +3 −37 plugins/funind/functional_principles_proofs.ml
  122. +0 −35 plugins/funind/functional_principles_types.ml
  123. +2 −3 plugins/funind/g_indfun.ml4
  124. +0 −38 plugins/funind/glob_term_to_relation.ml
  125. +1 −59 plugins/funind/indfun.ml
  126. +0 −13 plugins/funind/indfun_common.ml
  127. +0 −11 plugins/funind/merge.ml
  128. +0 −16 plugins/funind/recdef.ml
  129. +1 −3 plugins/micromega/certificate.ml
  130. +1 −2 plugins/micromega/csdpcert.ml
  131. +0 −3 plugins/micromega/g_micromega.ml4
  132. +2 −2 plugins/micromega/sos_lib.ml
  133. +0 −21 plugins/nsatz/nsatz.ml4
  134. +1 −2 plugins/nsatz/polynom.ml
  135. +1 −2 plugins/omega/PreOmega.v
  136. +0 −12 plugins/omega/coq_omega.ml
  137. +0 −2 plugins/omega/omega.ml
  138. +0 −1 plugins/quote/g_quote.ml4
  139. +0 −3 plugins/quote/quote.ml
  140. +0 −1 plugins/romega/const_omega.ml
  141. +0 −1 plugins/romega/refl_omega.ml
  142. +0 −10 plugins/rtauto/proof_search.ml
  143. +0 −9 plugins/rtauto/refl_tauto.ml
  144. +0 −16 plugins/setoid_ring/newring.ml4
  145. +0 −4 plugins/syntax/ascii_syntax.ml
  146. +0 −2 plugins/syntax/nat_syntax.ml
  147. +0 −1 plugins/syntax/numbers_syntax.ml
  148. +0 −6 plugins/syntax/r_syntax.ml
  149. +0 −7 plugins/syntax/string_syntax.ml
  150. +0 −2 plugins/xml/doubleTypeInference.ml
  151. +0 −134 plugins/xml/dumptree.ml4
  152. +0 −78 plugins/xml/proof2aproof.ml
  153. +0 −184 plugins/xml/proofTree2Xml.ml4
  154. +0 −3 plugins/xml/xml_plugin.mllib
  155. +3 −132 plugins/xml/xmlcommand.ml
  156. +0 −11 plugins/xml/xmlcommand.mli
  157. +1 −7 plugins/xml/xmlentries.ml4
  158. +0 −35 pretyping/cases.ml
  159. +1 −4 pretyping/classops.ml
  160. +0 −4 pretyping/evarconv.ml
  161. +0 −13 pretyping/evarutil.ml
  162. +0 −4 pretyping/evd.ml
  163. +8 −4 pretyping/matching.ml
  164. +8 −6 pretyping/matching.mli
  165. +4 −0 pretyping/pretype_errors.ml
  166. +4 −0 pretyping/pretype_errors.mli
  167. +0 −9 pretyping/pretyping.ml
  168. +0 −9 pretyping/program.ml
  169. +0 −2 pretyping/reductionops.ml
  170. +2 −2 pretyping/tacred.ml
  171. +0 −11 pretyping/term_dnet.ml
  172. +0 −6 pretyping/typeclasses.ml
  173. +0 −1 pretyping/typeclasses_errors.ml
  174. +11 −9 pretyping/unification.ml
  175. +1 −1 pretyping/unification.mli
  176. +4 −6 printing/ppconstr.ml
  177. +13 −35 printing/pptactic.ml
  178. +7 −4 printing/pptactic.mli
  179. +15 −0 printing/pputils.ml
  180. +2 −12 printing/{tactic_printer.mli → pputils.mli}
  181. +7 −12 printing/ppvernac.ml
  182. +0 −1 printing/printer.ml
  183. +1 −1 printing/printing.mllib
  184. +0 −169 printing/tactic_printer.ml
  185. +0 −18 proofs/logic.ml
  186. +0 −4 proofs/logic.mli
  187. +1 −5 proofs/pfedit.ml
  188. +1 −16 proofs/proof.ml
  189. +0 −4 proofs/proof.mli
  190. +0 −11 proofs/proof_global.ml
  191. +6 −47 proofs/proof_type.ml
  192. +8 −58 proofs/proof_type.mli
  193. +2 −2 proofs/proofview.ml
  194. +33 −50 proofs/refiner.ml
  195. +1 −12 proofs/refiner.mli
  196. +13 −17 proofs/tacmach.ml
  197. +0 −2 proofs/tacmach.mli
  198. +1 −1 scripts/coqc.ml
  199. +7 −16 scripts/coqmktop.ml
  200. +4 −49 tactics/auto.ml
  201. +0 −6 tactics/autorewrite.ml
  202. +25 −27 tactics/class_tactics.ml4
  203. +0 −7 tactics/eauto.ml4
  204. +4 −9 tactics/elim.ml
  205. +0 −16 tactics/elimschemes.ml
  206. +1 −8 tactics/eqdecide.ml4
  207. +0 −2 tactics/equality.ml
  208. +0 −4 tactics/extraargs.ml4
  209. +0 −9 tactics/extratactics.ml4
  210. +45 −88 tactics/hiddentac.ml
  211. +4 −5 tactics/hiddentac.mli
  212. +0 −15 tactics/hipattern.ml4
  213. +3 −3 tactics/inv.ml
  214. +0 −13 tactics/nbtermdn.ml
  215. +0 −13 tactics/rewrite.ml4
  216. +59 −72 tactics/tacinterp.ml
  217. +1 −0 tactics/tacticals.ml
  218. +2 −0 tactics/tacticals.mli
  219. +0 −5 tactics/tactics.ml
  220. +0 −2 tactics/tauto.ml4
  221. +1 −1 theories/FSets/FMapAVL.v
  222. +1 −1 theories/MSets/MSetGenTree.v
  223. +1 −1 theories/Numbers/Natural/Abstract/NStrongRec.v
  224. +1 −1 theories/Program/Subset.v
  225. +2 −2 theories/QArith/Qcanon.v
  226. +7 −7 tools/coq_makefile.ml
  227. +0 −13 tools/coqdoc/cpretty.mll
  228. +0 −35 tools/coqdoc/index.ml
  229. +0 −7 tools/coqdoc/output.ml
  230. +0 −2 tools/coqdoc/tokens.ml
  231. +0 −1 tools/coqwc.mll
  232. +0 −1 tools/gallina_lexer.mll
  233. +8 −1 toplevel/cerrors.ml
  234. +0 −3 toplevel/class.ml
  235. +0 −6 toplevel/classes.ml
  236. +0 −24 toplevel/command.ml
  237. +2 −0 toplevel/coqtop.ml
  238. +12 −15 toplevel/himsg.ml
  239. +7 −2 toplevel/ide_slave.ml
  240. +2 −2 toplevel/lemmas.ml
  241. +140 −81 toplevel/metasyntax.ml
  242. +11 −15 toplevel/{mltop.ml4 → mltop.ml}
  243. +1 −22 toplevel/obligations.ml
  244. +0 −7 toplevel/record.ml
  245. +0 −5 toplevel/search.ml
  246. +6 −7 toplevel/toplevel.ml
  247. +1 −0 toplevel/usage.ml
  248. +28 −5 toplevel/vernac.ml
  249. +3 −0 toplevel/vernac.mli
  250. +0 −1 toplevel/vernacinterp.ml
  251. +0 −5 toplevel/whelp.ml4
View
@@ -110,7 +110,7 @@ g_*.ml
ide/project_file.ml
lib/pp.ml
-lib/compat.ml
+parsing/compat.ml
grammar/q_util.ml
grammar/q_constr.ml
grammar/q_coqast.ml
@@ -136,15 +136,12 @@ tactics/eqdecide.ml
tactics/extratactics.ml
tactics/extraargs.ml
tools/coq_tex.ml
-toplevel/mltop.ml
toplevel/whelp.ml
ide/coqide_main.ml
ide/coqide_main_opt.ml
# other auto-generated files
-toplevel/mltop.optml
-toplevel/mltop.byteml
kernel/byterun/coq_jumptbl.h
kernel/copcodes.ml
scripts/tolink.ml
View
@@ -72,15 +72,26 @@ READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary
VALIDATE=
COQ_XML= # is "-xml" when building XML library
VM= # is "-no-vm" to not use the vm"
-TIMECMD= # is "'time -p'" to get compilation time of .v
-# NB: variable TIME, if set, is the formatting string for unix command 'time'.
-# For instance:
-# TIME="%C (%U user, %S sys, %e total, %M maxres)"
+TIMED= # non-empty will activate a default time command
+ # when compiling .v (see $(STDTIME) below)
+
+TIMECMD= # if you prefer a specific time command instead of $(STDTIME)
+ # e.g. "'time -p'"
+
+# NB: if you want to collect compilation timings of .v and import them
+# in a spreadsheet, I suggest something like:
+# make TIMED=1 2> timings.csv
+
+# NB: do not use a variable named TIME, since this variable controls
+# the output format of the unix command time. For instance:
+# TIME="%C (%U user, %S sys, %e total, %M maxres)"
+
+STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
COQOPTS=$(COQ_XML) $(VM)
-BOOTCOQTOP:=$(TIMECMD) $(COQTOPEXE) -boot $(COQOPTS)
-BOOTCOQC:=$(BOOTCOQTOP) -compile
+BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile
# The SHOW and HIDE variables control whether make will echo complete commands
# or only abbreviated versions.
@@ -117,15 +128,16 @@ endif
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
+SYSMOD:=str unix
+SYSCMA:=$(addsuffix .cma,$(SYSMOD))
+SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
+
ifeq ($(CAMLP4),camlp5)
-SYSMOD:=str unix gramlib
+P4CMA:=gramlib.cma
else
-SYSMOD:=str unix dynlink camlp4lib
+P4CMA:=dynlink.cma camlp4lib.cma
endif
-SYSCMA:=$(addsuffix .cma,$(SYSMOD))
-SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
-
###########################################################################
# Infrastructure for the rest of the Makefile
@@ -206,6 +218,9 @@ coqlight: theories-light tools coqbinaries
states: theories/Init/Prelude.vo
+miniopt: $(COQTOPEXE) pluginsopt
+minibyte: $(COQTOPBYTE) pluginsbyte
+
ifeq ($(BEST),opt)
$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
$(SHOW)'COQMKTOP -o $@'
@@ -442,7 +457,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
###########################################################################
.PHONY: plugins omega micromega setoid_ring nsatz xml extraction
-.PHONY: fourier funind cc rtauto btauto pluginsopt
+.PHONY: fourier funind cc rtauto btauto pluginsopt pluginsbyte
plugins: $(PLUGINSVO)
omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
@@ -458,6 +473,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMA)
btauto: $(BTAUTOVO) $(BTAUTOCMA)
pluginsopt: $(PLUGINSOPT)
+pluginsbyte: $(PLUGINS)
###########################################################################
# rules to make theories and plugins
@@ -663,12 +679,12 @@ install-latex:
source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -latex -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@
mli-doc:: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -html -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
@@ -681,9 +697,9 @@ ml-dot:: $(MLEXTRAFILES)
$(DOT) -Tpng $< -o $@
%_types.dot: %.mli
- $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+ $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
-OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
$(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
%.dot: | %.mllib.d
@@ -702,7 +718,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
$(OCAMLDOC_MLLIBD)
%.dot: %.mli
- $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+ $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
@@ -713,7 +729,7 @@ $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
dev/printers.cma: | dev/printers.mllib.d
$(SHOW)'Testing $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $(P4CMA) $^ -o test-printer
@rm -f test-printer
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
@@ -726,25 +742,6 @@ grammar/grammar.cma: | grammar/grammar.mllib.d
$(SHOW)'OCAMLC -a $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
-# toplevel/mltop.ml4 (ifdef Byte)
-
-## NB: mltop.ml correspond to the byte version (and hence need no special rules)
-## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d
-## as dependency file, be sure to import the same modules in the different sections
-## of the ml4
-
-toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml.d toplevel/mltop.ml4.d
- $(SHOW)'OCAMLOPT $<'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@
-
-toplevel/mltop.ml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
- $(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@
-
-toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here
- $(SHOW)'CAMLP4O $<'
- $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@
-
ide/coqide_main.ml: ide/coqide_main.ml4
$(SHOW)'CAMLP4O $<'
$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@
@@ -753,6 +750,18 @@ ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
$(SHOW)'CAMLP4O $<'
$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@
+# Specific rule for term.ml which uses -rectypes
+# Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
+
+TERM:=kernel/term
+
+$(TERM).cmo: $(TERM).ml | $(TERM).ml.d
+ $(SHOW)'OCAMLC -rectypes $<'
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -rectypes -c $<
+
+$(TERM).cmx: $(TERM).ml | $(TERM).ml.d
+ $(SHOW)'OCAMLOPT -rectypes $<'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
# pretty printing of the revision number when compiling a checked out
# source tree
View
@@ -81,7 +81,7 @@ SRCDIRS:=\
# Order is relevent here because kernel and checker contain files
# with the same name
-CHKSRCDIRS:= checker lib config kernel
+CHKSRCDIRS:= checker lib config kernel parsing
###########################################################################
# tools
@@ -225,7 +225,7 @@ IDEMOD:=$(shell cat ide/ide.mllib)
# coqmktop, coqc
COQENVCMO:=lib/clib.cma\
- lib/pp_control.cmo lib/compat.cmo lib/pp.cmo lib/loc.cmo lib/errors.cmo
+ lib/loc.cmo lib/errors.cmo
COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo
View
31 _tags
@@ -1,15 +1,15 @@
## tags for binaries
-<scripts/coqmktop.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
-<scripts/coqc.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<scripts/coqmktop.{native,byte}> : use_str, use_unix
+<scripts/coqc.{native,byte}> : use_str, use_unix
<tools/coqdep_boot.{native,byte}> : use_unix
-<tools/coqdep.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<tools/coqdep.{native,byte}> : use_str, use_unix
<tools/coq_tex.{native,byte}> : use_str
<tools/coq_makefile.{native,byte}> : use_str, use_unix
<tools/coqdoc/main.{native,byte}> : use_str
<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide
-<checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX
+<checker/main.{native,byte}> : use_str, use_unix
<plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix
<tools/mkwinapp.{native,byte}> : use_unix
<tools/fake_ide.{native,byte}> : use_unix
@@ -22,20 +22,13 @@
<grammar/grammar.{cma,cmxa}> : use_unix
-## tags for camlp4 files
+## tags for ml files
+
+"kernel/term.ml": rectypes
-"toplevel/mltop.ml4": is_mltop
+## tags for camlp4 files
"toplevel/whelp.ml4": use_grammar
-"parsing/g_obligations.ml4": use_grammar
-"tactics/extraargs.ml4": use_grammar
-"tactics/extratactics.ml4": use_grammar
-"tactics/class_tactics.ml4": use_grammar
-"tactics/eauto.ml4": use_grammar
-"tactics/tauto.ml4": use_grammar
-"tactics/eqdecide.ml4": use_grammar
-"tactics/hipattern.ml4": use_grammar, use_constr
-"tactics/rewrite.ml4": use_grammar
"parsing/g_constr.ml4": use_compat5
"parsing/g_ltac.ml4": use_compat5
@@ -45,15 +38,19 @@
"parsing/g_vernac.ml4": use_compat5
"parsing/g_xml.ml4": use_compat5
"parsing/pcoq.ml4": use_compat5
-"plugins/decl_mode/g_decl_mode.ml4": use_compat5
-"plugins/funind/g_indfun.ml4": use_compat5
+"parsing/g_obligations.ml4": use_grammar
"grammar/argextend.ml4": use_compat5b
"grammar/q_constr.ml4": use_compat5b
"grammar/tacextend.ml4": use_compat5b
"grammar/vernacextend.ml4": use_compat5b
+<tactics/*.ml4>: use_grammar
+"tactics/hipattern.ml4": use_constr
+
<plugins/**/*.ml4>: use_grammar
+"plugins/decl_mode/g_decl_mode.ml4": use_compat5
+"plugins/funind/g_indfun.ml4": use_compat5
## sub-directory inclusion
View
2 build
@@ -7,7 +7,7 @@ MYCFG=myocamlbuild_config.ml
export CAML_LD_LIBRARY_PATH=`pwd`/_build/kernel/byterun
check_config() {
- [ -f $MYCFG ] || (echo "please run ./configure first"; exit 1)
+ if [ ! -f $MYCFG ]; then echo "please run ./configure first"; exit 1; fi
}
ocb() { $OCAMLBUILD $FLAGS $*; }
View
@@ -1,6 +1,5 @@
Coq_config
Pp_control
-Compat
Flags
Pp
Loc
@@ -13,6 +12,7 @@ CList
CArray
Util
Option
+Hashset
Hashcons
CUnix
System
View
@@ -7,12 +7,7 @@
(************************************************************************)
open Pp
-open Errors
-open Util
-open System
-open Flags
open Names
-open Term
open Declarations
open Environ
View
@@ -12,7 +12,6 @@ open Util
open System
open Flags
open Names
-open Term
open Check
let () = at_exit flush_all
@@ -231,8 +230,6 @@ let rec explain_exn = function
hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
| Stream.Error txt ->
hov 0 (str "Syntax error: " ++ str txt)
- | Compat.Token.Error txt ->
- hov 0 (str "Syntax error: " ++ str txt)
| Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() )
| UserError(s,pps) ->
@@ -274,7 +271,7 @@ let rec explain_exn = function
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
- | Loc.Exc_located (loc,exc) ->
+ | Loc.Exc_located (loc, exc) ->
hov 0 ((if loc = Loc.ghost then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
++ explain_exn exc)
View
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
open Util
open Pp
open Term
View
@@ -1,4 +1,3 @@
-open Errors
open Util
open Names
open Term
@@ -111,7 +110,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
let mp_in_delta mp =
Deltamap.mem_mp mp
-let rec find_prefix resolve mp =
+let find_prefix resolve mp =
let rec sub_mp = function
| MPdot(mp,l) as mp_sup ->
(try Deltamap.find_mp mp_sup resolve
View
@@ -4,7 +4,6 @@ open Errors
open Util
open Names
open Term
-open Inductive
open Reduction
open Typeops
open Indtypes
View
@@ -11,10 +11,8 @@ open Errors
open Util
open Pp
open Names
-open Univ
open Term
open Declarations
-open Environ
(*i*)
let error_not_a_constant l =
View
@@ -8,7 +8,6 @@
open Errors
open Util
-open Names
open Term
open Univ
open Closure
Oops, something went wrong.

0 comments on commit 90867e6

Please sign in to comment.