diff options
| -rw-r--r-- | .travis.yml | 16 | ||||
| -rw-r--r-- | Makefile.doc | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 | ||||
| -rw-r--r-- | lib/system.ml | 3 | ||||
| -rw-r--r-- | parsing/doc.tex | 9 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 2 |
6 files changed, 17 insertions, 23 deletions
diff --git a/.travis.yml b/.travis.yml index f4f01d2f02..9ec936b0c9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -40,10 +40,10 @@ env: # system is == 4.02.3 - COMPILER="system" - COMPILER_BE="4.06.0" - - CAMLP5_VER="6.14" - - CAMLP5_VER_BE="7.03" - - FINDLIB_VER="1.4.1" - - FINDLIB_VER_BE="1.7.3" + - CAMLP5_VER=".6.14" + - CAMLP5_VER_BE=".7.03" + - FINDLIB_VER=".1.4.1" + - FINDLIB_VER_BE=".1.7.3" - LABLGTK="lablgtk.2.18.3 lablgtk-extras.1.6" - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" @@ -76,6 +76,8 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: + # ppx_tools_versioned requires a specific version findlib + - FINDLIB_VER="" - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - if: NOT (type = pull_request) env: @@ -221,7 +223,7 @@ matrix: env: - TEST_TARGET="test-suite" - COMPILER="4.02.3" - - CAMLP5_VER="6.17" + - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-local" before_install: @@ -234,7 +236,7 @@ matrix: env: - TEST_TARGET="" - COMPILER="4.02.3" - - CAMLP5_VER="6.17" + - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - EXTRA_CONF="-coqide opt -warn-error" @@ -264,7 +266,7 @@ install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config list -- opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind.${FINDLIB_VER} ${EXTRA_OPAM} +- opam install -j ${NJOBS} -y camlp5${CAMLP5_VER} ocamlfind${FINDLIB_VER} ${EXTRA_OPAM} - opam list script: diff --git a/Makefile.doc b/Makefile.doc index 8cb9c9f0fa..3385e4951d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -400,7 +400,7 @@ source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -latex -o $@' - $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\ + $(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\ $(DOCMLIS) -noheader -t "Coq mlis documentation" \ -intro $(OCAMLDOCDIR)/docintro -o $@.tmp $(SHOW)'OCAMLDOC utf8 fix' @@ -410,13 +410,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi) mli-doc: $(DOCMLIS:.mli=.cmi) $(SHOW)'OCAMLDOC -html' - $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \ $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ -css-style style.css ml-dot: $(MLFILES) - $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \ + $(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \ $(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot %_dep.png: %.dot @@ -449,7 +449,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex $(SHOW)'PDFLATEX $*.tex' $(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex) - $(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) + $(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log) ########################################################################### # local web server diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 66a5f107a5..9635b3ab1a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal \item applying the abstracted goal to {\term} \end{enumerate} -For instance, if the current goal $T$ is expressible has $\phi(t)$ +For instance, if the current goal $T$ is expressible as $\phi(t)$ where the notation captures all the instances of $t$ in $\phi(t)$, then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt x}$)$) $t$}. This command can be used, for instance, when the tactic diff --git a/lib/system.ml b/lib/system.ml index e56736eb15..0ad86c73ff 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -54,7 +54,8 @@ let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) -let trust_file_cache = ref true +(** Don't trust in interactive mode (the default) *) +let trust_file_cache = ref false let exists_in_dir_respecting_case dir bf = let cache_dir dir = diff --git a/parsing/doc.tex b/parsing/doc.tex deleted file mode 100644 index 68ab601cc1..0000000000 --- a/parsing/doc.tex +++ /dev/null @@ -1,9 +0,0 @@ - -\newpage -\section*{The Coq parsers and printers} - -\ocwsection \label{parsing} -This chapter describes the implementation of the \Coq\ parsers and printers. - -\bigskip -\begin{center}\epsfig{file=parsing.dep.ps}\end{center} diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 5b73471c59..a7065c0315 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -153,7 +153,7 @@ let add_compat_require opts v = let set_batch_mode opts = Flags.quiet := true; - System.trust_file_cache := false; + System.trust_file_cache := true; { opts with batch_mode = true } let add_compile opts verbose s = |