diff options
Diffstat (limited to 'dev')
27 files changed, 95 insertions, 81 deletions
diff --git a/dev/README b/dev/README index b446c3e974..6b83579def 100644 --- a/dev/README +++ b/dev/README @@ -1,4 +1,4 @@ -This directory contains informations and tools to help developing the +This directory contains information and tools to help develop the Coq system ====================== @@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the Debugging and profiling (in current directory - see doc/debugging.txt) ----------------------- -ocamldebug-coq: to launch ocaml debugger +ocamldebug-coq: to launch ocaml debugger (generated by the configure script) -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger +db: to install pretty-printers from ocaml debugger +base_db: to install raw pretty-printers from ocaml debugger -include: to install pretty-printers from ocaml toplevel +include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) base_include: to install raw pretty-printers from ocaml toplevel -vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging +vm_printers.ml, top_printers.ml: ML pretty-printers for debugging -Miscellaneous informations about the code (directory doc) +Miscellaneous information about the code (directory doc) ----------------------------------------- -changes.txt: (partial) per-version summary of the evolutions of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.txt: help for debugging or profiling -universes.txt: help to debug universes -translate.txt: help to use coq translator +changes.md: (partial) per-version summary of the evolution of Coq ML source +style.txt: a few style recommendations for writing Coq ML files +debugging.md: help for debugging or profiling +universes.txt: help for debugging universes +translate.txt: help for using coq translator extensions.txt: some help about TACTIC EXTEND -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation +header: standard header for Coq ML files +perf-analysis: analysis of perfs measured on the compilation of user contribs +cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) diff --git a/dev/base_include b/dev/base_include index d7059fe74f..2a4ad4a157 100644 --- a/dev/base_include +++ b/dev/base_include @@ -18,12 +18,10 @@ #directory "intf";; #directory "stm";; #directory "vernac";; -#directory "../API";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) -#load "API.cma";; #use "top_printers.ml";; #use "vm_printers.ml";; @@ -193,8 +191,8 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; -let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; +let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of implicit syntax *) diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index cfcc09b327..dc33838f1e 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -25,4 +25,4 @@ mkdir -p _build # Temporary countermeasure to hdiutil error 5341 # head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg +hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index f12cbe0a78..c467678215 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1087,7 +1087,7 @@ function copy_coq_license { install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" + install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" @@ -1174,7 +1174,7 @@ function make_mingw_make { if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then # The config.h.win32 file is fine - don't edit it # We need to copy the mingw gcc here as "gcc" - then the batch file will use it - cp /usr/bin/${ARCH}-w64-mingw32-gcc-5.4.0.exe ./gcc.exe + cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe # By some magic cygwin bash can run batch files logn build ./build_w32.bat gcc # Copy make to Coq folder diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 48f1d3759b..2c2f0fa47c 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -15,7 +15,7 @@ SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here -!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" +!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index e2fbf1f6d1..dec6f0d182 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -25,7 +25,7 @@ if %USEOPAM% == false ( -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit - 7z a coq-opensource-archive-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit ) if %USEOPAM% == true ( @@ -37,5 +37,5 @@ if %USEOPAM% == true ( GOTO :EOF :ErrorExit - ECHO ERROR MakeCoq_MinGW.bat failed + ECHO ERROR %0 failed EXIT /b 1 diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 23131c94c6..58c90ff11d 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -5,8 +5,17 @@ set -xe if [ -n "${GITLAB_CI}" ]; then export COQBIN=`pwd`/_install_ci/bin - export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME" + export CI_BRANCH="$CI_COMMIT_REF_NAME" else + if [ -n "${TRAVIS}" ]; + then + export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" + export CI_BRANCH="$TRAVIS_BRANCH" + elif [ -n "${CIRCLECI}" ]; + then + export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" + export CI_BRANCH="$CIRCLE_BRANCH" + fi export COQBIN=`pwd`/bin fi export PATH="$COQBIN:$PATH" diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index af4a96f4ae..7716bcb59a 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,4 +1,4 @@ -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi diff --git a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh deleted file mode 100644 index 5c4dd1324f..0000000000 --- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then - formal_topology_CI_BRANCH=ci - formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git - - HoTT_CI_BRANCH=coq-pr-1033 - HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git - - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh deleted file mode 100644 index cdca8e525a..0000000000 --- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then - ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer - ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git -fi diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh deleted file mode 100644 index 6741cf26fb..0000000000 --- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then - ltac2_CI_BRANCH=master - ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2 -fi diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh deleted file mode 100644 index c9f1272bed..0000000000 --- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then - ltac2_CI_BRANCH=localityfixyou - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git -fi diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh deleted file mode 100644 index 68e1901f7f..0000000000 --- a/dev/ci/user-overlays/06217-coqdep-at-once.sh +++ /dev/null @@ -1,3 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then - UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git -fi diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh deleted file mode 100644 index 7e9b5febdd..0000000000 --- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then - Equations_CI_BRANCH=fix-coq-6324 - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh deleted file mode 100644 index c0dcf79e1d..0000000000 --- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then - Equations_CI_BRANCH=econstr+fix_class - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh new file mode 100644 index 0000000000..c2e3670380 --- /dev/null +++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then + Equations_CI_BRANCH=rm-local-polymorphic-flag + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh deleted file mode 100644 index 8aea7dee3a..0000000000 --- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then - Equations_CI_BRANCH=interp+less_impstyle_p2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh new file mode 100644 index 0000000000..9677b35253 --- /dev/null +++ b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then + Equations_CI_BRANCH=API-removal + Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git + coq_dpdgraph_CI_BRANCH=API-removal + coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git + ltac2_CI_BRANCH=API-removal + ltac2_CI_GITURL=https://github.com/gares/ltac2.git +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9146d3d521..9f0377ceea 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` -if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then +if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git fi ``` + +(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh)) diff --git a/dev/core.dbg b/dev/core.dbg index 18e82c352c..00a4355a48 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -17,5 +17,4 @@ load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer intf.cma -load_printer API.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 01aa6b599b..e616bd5663 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find a correspondence table [here](/dev/bugzilla2github_stripped.csv). All the other bugs kept their number. -### Plugin API - -Coq 8.8 offers a new module overlay containing a proposed plugin API -in `API/API.ml`; this overlay is enabled by adding the `-open API` -flag to the OCaml compiler; this happens automatically for -developments in the `plugin` folder and `coq_makefile`. - -However, `coq_makefile` can be instructed not to enable this flag by -passing `-bypass-API`. - ### ML API General deprecation @@ -68,6 +58,13 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### XML IDE Protocol + +- Before 8.8, `Query` only executed the first command present in the + `query` string; starting with 8.8, the caller may include several + statements. This is useful for instance for temporarily setting an + option and then executing a command. + ## Changes between Coq 8.6 and Coq 8.7 ### Ocaml diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fa145d498a..fd3cbd1bc3 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism printers too. -Debugging from Caml debugger -============================ +Debugging with ocamldebug from Emacs +==================================== Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\ Coq must be configured with `-local` (`./configure -local`) and the @@ -59,6 +59,29 @@ Debugging from Caml debugger from the debugger. If this happens, unset the variable, re-start Emacs, and run the debugger again. +Debugging with ocamldebug from the command line +=============================================== + +In the `coq` directory: +1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq. +2. Run `make` (to compile the .v files) +3. Run `make byte` +4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH. + Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH. (The + CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.) +5. Run `dev/ocamldebug-coq bin/coqtop.byte` (on Cygwin/Windows, use `... bin/coqtop.byte.exe`) +6. Enter `source db` to load printers +7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc. +8. See the ocamldebug manual for more information. A few points: + - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml). + `break` can be abbreviated as `b`. + - `backtrace` or `bt` to see the call stack + - `step` or `s` goes into called functions; `next` or `n` skips over them + - `list` or `li` shows the code just before and after the current stack frame + - `print <var>` or `p <var>` to see the value of a variable +Note that `make byte` doesn't recompile .v files. `make` recompiles all of them if there +are changes in any .ml file--safer but much slower. + Global gprof-based profiling ============================ diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 18f6288f6f..b35571e9ca 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`. <string>${message}</string> </value> ``` + +Before 8.8, `Query` only executed the first command present in the +`query` string; starting with 8.8, the caller may include several +statements. This is useful for instance for temporarily setting an +option and then executing a command. + ------------------------------- diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index 80da845174..f48013cf2e 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -13,7 +13,7 @@ SetCompressor lzma !define MY_PRODUCT "Coq" ;Define your own software name here !define COQ_SRC_PATH "..\.." -!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe" +!define OUTFILE "coq-${VERSION}-installer-windows-${ARCH}.exe" !include "MUI2.nsh" !include "FileAssociation.nsh" diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f4799f7b2c..3850c05fd9 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -23,7 +23,6 @@ exec $OCAMLDEBUG \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ - -I $COQTOP/API \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \ -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \ diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index 4c4dbe1e97..d7acf01f1d 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,10 +1,11 @@ #!/usr/bin/env bash -# Usage: dev/tools/backport-pr.sh <PR number> +# Usage: dev/tools/backport-pr.sh <PR number> [--stop-before-merging] set -e PRNUM=$1 +OPTION=$2 if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then echo "PR #${PRNUM} does not exist." @@ -49,6 +50,10 @@ else fi +if [[ "${OPTION}" == "--stop-before-merging" ]]; then + exit 0 +fi + git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" git branch -d ${BRANCH} diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 832040ad2c..ff38257877 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -233,7 +233,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x)) +let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) |