diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/README | 30 | ||||
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rwxr-xr-x | dev/build/osx/make-macos-dmg.sh | 2 | ||||
| -rw-r--r-- | dev/build/windows/patches_coq/coq_new.nsi | 2 | ||||
| -rw-r--r-- | dev/ci/README.md | 2 | ||||
| -rw-r--r-- | dev/ci/appveyor.bat | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh | 4 | ||||
| -rw-r--r-- | dev/db | 95 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 27 | ||||
| -rw-r--r-- | dev/include | 1 | ||||
| -rwxr-xr-x | dev/nsis/coq.nsi | 2 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
| -rw-r--r-- | dev/set_raw_db | 1 | ||||
| -rwxr-xr-x | dev/tools/backport-pr.sh | 7 | ||||
| -rwxr-xr-x | dev/tools/github-check-prs.py | 47 | ||||
| -rw-r--r-- | dev/top_printers.ml | 15 | ||||
| -rw-r--r-- | dev/top_printers.mli | 173 |
17 files changed, 339 insertions, 75 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 2a4ad4a157..472c0c605e 100644 --- a/dev/base_include +++ b/dev/base_include @@ -52,7 +52,7 @@ #install_printer ppvblock;; #install_printer (* bigint *) ppbigint;; #install_printer (* loc *) pploc;; -#install_printer (* substitution *) prsubst;; +#install_printer (* substitution *) ppsubst;; (* Open main files *) 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/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/README.md b/dev/ci/README.md index f4423558cc..bb13587e94 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index 72ee89962c..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 ( diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 0000000000..78789a6fc5 --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi @@ -1,37 +1,67 @@ source core.dbg load_printer top_printers.cmo +install_printer Top_printers.pP install_printer Top_printers.ppfuture - install_printer Top_printers.ppid -install_printer Top_printers.ppidset -install_printer Top_printers.ppevar -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppintset install_printer Top_printers.pplab -install_printer Top_printers.ppdir install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir install_printer Top_printers.ppmp -install_printer Top_printers.ppkn install_printer Top_printers.ppcon -install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppproj +install_printer Top_printers.ppkn install_printer Top_printers.ppmind +install_printer Top_printers.ppind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid install_printer Top_printers.ppclindex -install_printer Top_printers.ppbigint -install_printer Top_printers.pp_transparent_state - -install_printer Top_printers.pppattern -install_printer Top_printers.ppglob_constr - +install_printer Top_printers.ppscheme +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof install_printer Top_printers.ppuni -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context @@ -40,34 +70,19 @@ install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst install_printer Top_printers.ppuniverse_level_subst install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future install_printer Top_printers.ppcumulativity_info install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.pptype -install_printer Top_printers.ppj -install_printer Top_printers.ppenv +install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t - -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.ppproofview -install_printer Top_printers.pphintdb - +install_printer Top_printers.ppenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc -install_printer Top_printers.prsubst -install_printer Top_printers.prdelta -install_printer Top_printers.ppfconstr +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument install_printer Top_printers.ppgenarginfo install_printer Top_printers.ppgenargargt install_printer Top_printers.ppist -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppididmap -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr 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/include b/dev/include index 0d34595f4f..b982f4c9fa 100644 --- a/dev/include +++ b/dev/include @@ -36,7 +36,6 @@ #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; #install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverse;; #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; 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 3850c05fd9..3cbccab44c 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,7 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ -I $CAMLP4LIB -I +threads \ -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ diff --git a/dev/set_raw_db b/dev/set_raw_db deleted file mode 100644 index 5caff7e5d4..0000000000 --- a/dev/set_raw_db +++ /dev/null @@ -1 +0,0 @@ -install_printer Top_printers.ppconstrdb 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/tools/github-check-prs.py b/dev/tools/github-check-prs.py new file mode 100755 index 0000000000..beb26d9104 --- /dev/null +++ b/dev/tools/github-check-prs.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 + +# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance +# debian package: python3-github +# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py +from github import Github +import argparse + +REPO = "coq/coq" +REBASE_LABEL="needs: rebase" + +parser = argparse.ArgumentParser() +parser.add_argument("--token-file", type=argparse.FileType('r')) +args = parser.parse_args() + +if args.token_file is None: + token = input("Github access token: ").strip() +else: + token = args.token_file.read().rstrip("\n") + args.token_file.close() + +if token == "": + print ("Warning: using the GitHub API without a token") + print ("We may run into rate limit issues") + g = Github() +else: + g = Github(token) + +repo = g.get_repo(REPO) + +for pull in repo.get_pulls(): + # if conflicts then dirty + # otherwise blocked (because I have no rights) + dirty = pull.mergeable_state == "dirty" + labelled = False + for label in repo.get_issue(pull.number).get_labels(): + if label.name == REBASE_LABEL: + labelled = True + if labelled and not dirty: + print ("PR #" + str(pull.number) + " is not dirty but is labelled") + print ("("+ pull.html_url +")") + elif dirty and not labelled: + print ("PR #" + str(pull.number) + " is dirty and not labelled") + print ("("+ pull.html_url +")") + else: + # give some feedback so the user can see we didn't crash + print ("PR #" + str(pull.number) + " OK") diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ff38257877..af38ce4b8c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -50,13 +50,13 @@ let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Classops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) -let pprecarg = function +let prrecarg = function | Declarations.Norec -> str "Norec" | Declarations.Mrec (mind,i) -> str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" | Declarations.Imbr (mind,i) -> str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) +let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) (* term printers *) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma @@ -65,8 +65,6 @@ let ppevar evk = pp (Evar.print evk) let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) -let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) @@ -111,7 +109,7 @@ let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> - str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") + str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") l open Ltac_pretype let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = @@ -149,8 +147,8 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) let ppj j = pp (genppj (envpp pr_ljudge_env) j) -let prsubst s = pp (Mod_subst.debug_pr_subst s) -let prdelta s = pp (Mod_subst.debug_pr_delta s) +let ppsubst s = pp (Mod_subst.debug_pr_subst s) +let ppdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) @@ -200,9 +198,8 @@ let pppftreestate p = pp(print_pftreestate p) let pproof p = pp(Proof.pr_proof p) -let ppuni u = pp(pr_uni u) +let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]") let prlev = Universes.pr_with_global_universes let ppuniverse_set l = pp (LSet.pr prlev l) diff --git a/dev/top_printers.mli b/dev/top_printers.mli new file mode 100644 index 0000000000..7b5e4a0b64 --- /dev/null +++ b/dev/top_printers.mli @@ -0,0 +1,173 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Printers for the ocaml toplevel. *) + +val pp : Pp.t -> unit +val pP : Pp.t -> unit (* with surrounding box *) + +val ppfuture : 'a Future.computation -> unit + +val ppid : Names.Id.t -> unit +val pplab : Names.Label.t -> unit +val ppmbid : Names.MBId.t -> unit +val ppdir : Names.DirPath.t -> unit +val ppmp : Names.ModPath.t -> unit +val ppcon : Names.Constant.t -> unit +val ppproj : Names.Projection.t -> unit +val ppkn : Names.KerName.t -> unit +val ppmind : Names.MutInd.t -> unit +val ppind : Names.inductive -> unit + +val ppsp : Libnames.full_path -> unit +val ppqualid : Libnames.qualid -> unit + +val ppclindex : Classops.cl_index -> unit + +val ppscheme : 'a Ind_tables.scheme_kind -> unit + +val prrecarg : Declarations.recarg -> Pp.t +val ppwf_paths : Declarations.recarg Rtree.t -> unit + +val pr_evar : Evar.t -> Pp.t +val ppevar : Evar.t -> unit + +(* Multiple printers for Constr.t *) +val ppconstr : Constr.t -> unit (* by Termops printer *) +val ppconstr_univ : Constr.t -> unit + +(* Extern as type *) +val pptype : Constr.types -> unit + +val ppsconstr : Constr.constr Mod_subst.substituted -> unit +val ppeconstr : EConstr.constr -> unit (* Termops printer *) +val ppconstr_expr : Constrexpr.constr_expr -> unit +val ppglob_constr : 'a Glob_term.glob_constr_g -> unit +val pppattern : Pattern.constr_pattern -> unit +val ppfconstr : CClosure.fconstr -> unit + +val ppbigint : Bigint.bigint -> unit + +val ppintset : Int.Set.t -> unit +val ppidset : Names.Id.Set.t -> unit + +val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t +val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit + +val pridmapgen : 'a Names.Id.Map.t -> Pp.t +val ppidmapgen : 'a Names.Id.Map.t -> unit + +val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t +val ppididmap : Names.Id.t Names.Id.Map.t -> unit + +val prconstrunderbindersidmap : + (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> Pp.t +val ppconstrunderbindersidmap : + (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> unit + +val ppevarsubst : + (Constr.t * Constr.t option * Names.Id.Map.key) list Names.Id.Map.t -> unit + +val ppunbound_ltac_var_map : + 'a Genarg.generic_argument Names.Id.Map.t -> unit + +val pr_closure : Ltac_pretype.closure -> Pp.t +val pr_closed_glob_constr_idmap : + Ltac_pretype.closed_glob_constr Names.Id.Map.t -> Pp.t +val pr_closed_glob_constr : Ltac_pretype.closed_glob_constr -> Pp.t +val ppclosure : Ltac_pretype.closure -> unit +val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit +val ppclosedglobconstridmap : + Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit + +val ppglobal : Globnames.global_reference -> unit + +val ppconst : + Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit +val ppvar : Names.Id.t * Constr.constr -> unit + +val genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t +val ppj : EConstr.unsafe_judgment -> unit + +val ppsubst : Mod_subst.substitution -> unit +val ppdelta : Mod_subst.delta_resolver -> unit + +val pp_idpred : Names.Id.Pred.t -> unit +val pp_cpred : Names.Cpred.t -> unit +val pp_transparent_state : Names.transparent_state -> unit + +val pp_stack_t : Constr.t Reductionops.Stack.t -> unit +val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit +val pp_state_t : Reductionops.state -> unit + +val ppmetas : Evd.Metaset.t -> unit +val ppevm : Evd.evar_map -> unit +val ppevmall : Evd.evar_map -> unit + +val pr_existentialset : Evar.Set.t -> Pp.t +val ppexistentialset : Evar.Set.t -> unit + +val ppexistentialfilter : Evd.Filter.t -> unit + +val ppclenv : Clenv.clausenv -> unit + +val ppgoalgoal : Goal.goal -> unit + +val ppgoal : Proof_type.goal Evd.sigma -> unit +(* also print evar map *) +val ppgoalsigma : Proof_type.goal Evd.sigma -> unit + +val pphintdb : Hints.Hint_db.t -> unit +val ppproofview : Proofview.proofview -> unit +val ppopenconstr : Evd.open_constr -> unit + +val pproof : Proof.t -> unit + +(* Universes *) +val ppuni : Univ.Universe.t -> unit +val ppuni_level : Univ.Level.t -> unit (* raw *) +val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) +val ppuniverse_set : Univ.LSet.t -> unit +val ppuniverse_instance : Univ.Instance.t -> unit +val ppuniverse_context : Univ.UContext.t -> unit +val ppuniverse_context_set : Univ.ContextSet.t -> unit +val ppuniverse_subst : Univ.universe_subst -> unit +val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit +val ppuniverse_level_subst : Univ.universe_level_subst -> unit +val ppevar_universe_context : UState.t -> unit +val ppconstraints : Univ.Constraint.t -> unit +val ppuniverseconstraints : Universes.Constraints.t -> unit +val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit +val ppcumulativity_info : Univ.CumulativityInfo.t -> unit +val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit +val ppuniverses : UGraph.t -> unit + +val ppnamedcontextval : Environ.named_context_val -> unit +val ppenv : Environ.env -> unit +val ppenvwithcst : Environ.env -> unit + +val pptac : Tacexpr.glob_tactic_expr -> unit + +val ppobj : Libobject.obj -> unit + +(* Some super raw printers *) +val cast_kind_display : Constr.cast_kind -> string +val constr_display : Constr.constr -> unit +val print_pure_constr : Constr.types -> unit + +val pploc : Loc.t -> unit + +val pp_argument_type : Genarg.argument_type -> unit +val pp_generic_argument : 'a Genarg.generic_argument -> unit + +val prgenarginfo : Geninterp.Val.t -> Pp.t +val ppgenarginfo : Geninterp.Val.t -> unit + +val ppgenargargt : ('a, 'b, 'c) Genarg.ArgT.tag -> unit + +val ppist : Geninterp.interp_sign -> unit |