diff options
Diffstat (limited to 'dev')
32 files changed, 334 insertions, 81 deletions
diff --git a/dev/Makefile.oug b/dev/Makefile.oug deleted file mode 100644 index ee69ea80df..0000000000 --- a/dev/Makefile.oug +++ /dev/null @@ -1,74 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### - - -#### Source Code Analysis via Oug #### -#### Cf http://home.gna.org/oug #### - - -# To be used from top dir : make -f dev/Makefile.oug ... - -include Makefile.build - -# Oug location: in the path by default, native version - -OUG:=oug.x - -# NB: coq should have been compiled with the same ocaml version as oug - -# NOTA: it seems we obtain more useless elements reported when _not_ -# providing the .mli files, and also when giving a precise start point. -# TO BE INVESTIGATED - -ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d)))) -local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1))) -mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i)) - -# Analysis of coqtop, without plugins - -COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA)) -COREMLI:=$(call mli_of_ml,$(COREML)) - -core.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) - -core.useless: core.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -core_intf.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI) - -core_intf.useless: core_intf.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -# Analysis of coqchk, considering only files in the checker/ subdir - -CHECKERML:=$(call local_ml_of_cma,checker/check.cma) -CHECKERMLI:=$(call mli_of_ml,$(CHECKERML)) - -## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS -MYCHKINCL:=$(MLINCLUDES) -I checker - -checker.oug: - $(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI) - -checker.useless: checker.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@ - -# Analysis of extraction - -EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA)) -EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI)) - -extraction.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI) - -extraction.useless: extraction.oug - $(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@ - -# More to come ...
\ No newline at end of file diff --git a/dev/base_include b/dev/base_include index 0abcefc38e..242405ae29 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,7 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/build/windows/MakeCoq_86_abs_ocaml.bat b/dev/build/windows/MakeCoq_86_abs_ocaml.bat new file mode 100644 index 0000000000..50483c4d4a --- /dev/null +++ b/dev/build/windows/MakeCoq_86_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86_abs ^
+ -destcoq=%ROOTPATH%\coq64_86_abs
diff --git a/dev/build/windows/MakeCoq_86_installer.bat b/dev/build/windows/MakeCoq_86_installer.bat new file mode 100644 index 0000000000..263520ff14 --- /dev/null +++ b/dev/build/windows/MakeCoq_86_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86_inst ^
+ -destcoq=%ROOTPATH%\coq64_86_inst
diff --git a/dev/build/windows/MakeCoq_86_installer_32.bat b/dev/build/windows/MakeCoq_86_installer_32.bat new file mode 100644 index 0000000000..14921dd7c3 --- /dev/null +++ b/dev/build/windows/MakeCoq_86_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86_inst ^
+ -destcoq=%ROOTPATH%\coq32_86_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat new file mode 100644 index 0000000000..914c332f46 --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_abs ^
+ -destcoq=%ROOTPATH%\coq64_86beta1_abs
diff --git a/dev/build/windows/MakeCoq_86beta1_installer.bat b/dev/build/windows/MakeCoq_86beta1_installer.bat new file mode 100644 index 0000000000..76a5bb35ac --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq64_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86beta1_installer_32.bat b/dev/build/windows/MakeCoq_86beta1_installer_32.bat new file mode 100644 index 0000000000..f53232b651 --- /dev/null +++ b/dev/build/windows/MakeCoq_86beta1_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6beta1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86beta1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86beta1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat new file mode 100644 index 0000000000..c0669f01d2 --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_abs_ocaml.bat @@ -0,0 +1,10 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -mode=absolute ^
+ -ocaml=Y ^
+ -make=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_abs ^
+ -destcoq=%ROOTPATH%\coq64_86rc1_abs
diff --git a/dev/build/windows/MakeCoq_86rc1_installer.bat b/dev/build/windows/MakeCoq_86rc1_installer.bat new file mode 100644 index 0000000000..66234ebbde --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_installer.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq64_86rc1_inst
diff --git a/dev/build/windows/MakeCoq_86rc1_installer_32.bat b/dev/build/windows/MakeCoq_86rc1_installer_32.bat new file mode 100644 index 0000000000..96f43e16a5 --- /dev/null +++ b/dev/build/windows/MakeCoq_86rc1_installer_32.bat @@ -0,0 +1,8 @@ +call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=32 ^
+ -installer=Y ^
+ -coqver=8.6rc1 ^
+ -destcyg=%ROOTPATH%\cygwin_coq32_86rc1_inst ^
+ -destcoq=%ROOTPATH%\coq32_86rc1_inst
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh new file mode 100755 index 0000000000..78ae7f02f9 --- /dev/null +++ b/dev/ci/ci-color.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +svn checkout https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color color + +( cd color && make -j ${NJOBS} ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh new file mode 100644 index 0000000000..412da626fd --- /dev/null +++ b/dev/ci/ci-common.sh @@ -0,0 +1,52 @@ +#!/bin/bash + +set -xe + +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN=`pwd`/bin/ +export PATH=`pwd`/bin:$PATH + +ls `pwd`/bin + +# Maybe we should just use Ruby... +mathcomp_CI_BRANCH=master +mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git + +# git_checkout branch +git_checkout() +{ + local _BRANCH=${1} + local _URL=${2} + local _DEST=${3} + + echo "Checking out ${_DEST}" + git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} + ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) +} + +checkout_mathcomp() +{ + git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + checkout_mathcomp math-comp + ( cd math-comp/mathcomp && \ + sed -i.bak '/ssrtest/d' Make && \ + sed -i.bak '/odd_order/d' Make && \ + sed -i.bak '/all\/all.v/d' Make && \ + sed -i.bak '/character/d' Make && \ + sed -i.bak '/real_closed/d' Make && \ + sed -i.bak '/solvable/d' Make && \ + sed -i.bak '/field/d' Make && \ + sed -i.bak '/fingroup/d' Make && \ + sed -i.bak '/algebra/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + + echo -en 'travis_fold:end:ssr.install\\r' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh new file mode 100755 index 0000000000..ec09389f8e --- /dev/null +++ b/dev/ci/ci-compcert.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +CompCert_CI_BRANCH=master +CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git + +opam install -j ${NJOBS} -y menhir +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert + +# Patch to avoid the upper version limit +( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh new file mode 100755 index 0000000000..94bd5e468f --- /dev/null +++ b/dev/ci/ci-coquelicot.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +install_ssreflect + +# Setup coquelicot +git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot + +( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh new file mode 100755 index 0000000000..18d7561804 --- /dev/null +++ b/dev/ci/ci-cpdt.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +wget http://adam.chlipala.net/cpdt/cpdt.tgz +tar xvfz cpdt.tgz + +( cd cpdt && make clean && make -j ${NJOBS} ) + diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh new file mode 100755 index 0000000000..c669195ddd --- /dev/null +++ b/dev/ci/ci-fiat-crypto.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto + +( cd fiat-crypto && make -j ${NJOBS} ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh new file mode 100755 index 0000000000..345924e40a --- /dev/null +++ b/dev/ci/ci-flocq.sh @@ -0,0 +1,9 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq + +( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh new file mode 100755 index 0000000000..ce870e52b5 --- /dev/null +++ b/dev/ci/ci-geocoq.sh @@ -0,0 +1,16 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +# XXX: replace by generic template +GeoCoq_CI_BRANCH=master +GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git + +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq + +( cd GeoCoq && \ + ./configure.sh && \ + sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + coq_makefile -f Make -o Makefile && \ + make -j ${NJOBS} ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh new file mode 100755 index 0000000000..0c07564c02 --- /dev/null +++ b/dev/ci/ci-hott.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT + +( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh new file mode 100755 index 0000000000..c21af976f4 --- /dev/null +++ b/dev/ci/ci-iris-coq.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +install_ssreflect + +# Setup stdpp +git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp + +( cd coq-stdpp && make -j ${NJOBS} && make install ) + +# Setup Iris +git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq + +( cd iris-coq && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh new file mode 100755 index 0000000000..4450dc0710 --- /dev/null +++ b/dev/ci/ci-math-classes.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes +( cd math-classes && make -j ${NJOBS} && make install ) + +git_checkout v8.6 https://github.com/c-corn/corn.git corn +( cd corn && make -j ${NJOBS} ) + diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh new file mode 100755 index 0000000000..2eb150cb52 --- /dev/null +++ b/dev/ci/ci-math-comp.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +checkout_mathcomp math-comp + +# odd_order takes too much time for travis. +( cd math-comp/mathcomp && \ + sed -i.bak '/PFsection/d' Make && \ + sed -i.bak '/stripped_odd_order_theorem/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh new file mode 100755 index 0000000000..91a33695b0 --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,16 @@ +#!/bin/bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +# MetaCoq + UniCoq + +git_checkout master https://github.com/unicoq/unicoq.git unicoq + +( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) + +git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq + +( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) + diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh new file mode 100755 index 0000000000..5e41211f1a --- /dev/null +++ b/dev/ci/ci-sf.sh @@ -0,0 +1,11 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +wget https://www.cis.upenn.edu/~bcpierce/sf/current/sf.tgz +tar xvfz sf.tgz + +( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} ) + + diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh new file mode 100755 index 0000000000..b946324924 --- /dev/null +++ b/dev/ci/ci-tlc.sh @@ -0,0 +1,8 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc + +( cd tlc && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 0000000000..15e619acbb --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_BRANCH=master +UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath + +( cd UniMath && \ + sed -i.bak '/Folds/d' Makefile && \ + sed -i.bak '/HomologicalAlgebra/d' Makefile && \ + make -j ${NJOBS} BUILD_COQ=no ) + diff --git a/dev/core.dbg b/dev/core.dbg index 38b9b29463..698db63d23 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -12,6 +12,7 @@ load_printer proofs.cma load_printer parsing.cma load_printer printing.cma load_printer tactics.cma +load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..8d2d055908 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,24 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The folder itself has been turned into a plugin. This does not change much, +but because it is a packed plugin, it may wreak havoc for third-party plugins +depending on any module defined in the ltac/ directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +an error of the form: + +Error: while loading myplugin.cmxs, no implementation available for Foo. + +In particular, most EXTEND macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement "open Ltac_plugin" +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not +work for EXTEND macros though. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For diff --git a/dev/include b/dev/include index 9068688f19..0f43f00729 100644 --- a/dev/include +++ b/dev/include @@ -61,7 +61,7 @@ (*#install_printer (* hints_path *) pphintspath;;*) #install_printer (* goal *) ppgoal;; (*#install_printer (* sigma goal *) ppsigmagoal;;*) -(*#install_printer (* proof *) pproof;;*) +#install_printer (* proof *) pproof;; #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* proofview *) ppproofview;; #install_printer (* metaset.t *) ppmetas;; diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 46caca8d6f..3850c05fd9 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -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/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/plugins/cc -I $COQTOP/plugins/dp \ @@ -32,6 +32,6 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ "$@" diff --git a/dev/top_printers.ml b/dev/top_printers.ml index b552d99949..dc354b130b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -200,7 +200,8 @@ let pppftreestate p = pp(print_pftreestate p) (* let ppsigmagoal g = pp(pr_goal (sig_it g)) *) (* let prgls gls = pp(pr_gls gls) *) (* let prglls glls = pp(pr_glls glls) *) -(* let pproof p = pp(print_proof Evd.empty empty_named_context p) *) + +let pproof p = pp(Proof.pr_proof p) let ppuni u = pp(pr_uni u) let ppuni_level u = pp (Level.pr u) @@ -233,7 +234,7 @@ let ppenvwithcst e = pp str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") -let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (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) |