diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-coq_performance_tests.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh | 6 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 |
4 files changed, 8 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index 67ea3a1fa1..1f14fc2941 100644 --- a/dev/base_include +++ b/dev/base_include @@ -114,7 +114,6 @@ open Logic open Proof open Proof_using open Redexpr -open Refiner open Tacmach open Hints diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh index 4eb77cfb24..fde8df8e3d 100755 --- a/dev/ci/ci-coq_performance_tests.sh +++ b/dev/ci/ci-coq_performance_tests.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download coq_performance_tests -( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf && make validate && make install ) +( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf-Sanity && make validate && make install ) diff --git a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh new file mode 100644 index 0000000000..c8c5b3ed5a --- /dev/null +++ b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12599" ] || [ "$CI_BRANCH" = "rm-deprecated-refiner" ]; then + + equations_CI_REF=rm-deprecated-refiner + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index bca1eb5754..f14edec639 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -186,7 +186,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with let ppclenv clenv = pp(pr_clenv clenv) let ppgoalgoal gl = pp(Goal.pr_goal gl) let ppgoal g = pp(Printer.pr_goal g) -let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g)) +let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Tacmach.project g)) let pphintdb db = pp(envpp Hints.pr_hint_db_env db) let ppproofview p = let gls,sigma = Proofview.proofview p in |