aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/ReadMe.txt2
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh12
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile5
-rw-r--r--dev/include_printers1
-rw-r--r--dev/top_printers.dbg1
-rw-r--r--dev/top_printers.ml1
-rw-r--r--dev/top_printers.mli1
7 files changed, 9 insertions, 14 deletions
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 052014824f..f34bbea4e9 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -423,7 +423,7 @@ Binary file ./bin/ocpp5.exe matches
Binary file ./lib/config/coq_config.cmo matches
Binary file ./lib/config/coq_config.o matches
Binary file ./lib/grammar/grammar.cma matches
-Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/ide/coqide/ide_win32_stubs.o matches
Binary file ./lib/lib/clib.a matches
Binary file ./lib/lib/clib.cma matches
Binary file ./lib/libcoqrun.a matches
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 963b0e6387..ba552ab302 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1303,11 +1303,11 @@ function copy_coq_gtk {
install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled" "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
install_glob "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
- install -D -T "ide/coq.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
- install -D -T "ide/coq-ssreflect.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+ install -D -T "ide/coqide/coq.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+ install -D -T "ide/coqide/coq-ssreflect.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
install_glob "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles"
- install -D -T "ide/coq_style.xml" "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+ install -D -T "ide/coqide/coq_style.xml" "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
install_rec "$PREFIXMINGW/share/themes" '*' "$PREFIXCOQ/share/themes"
@@ -1340,8 +1340,8 @@ function copy_coq_gtk {
# COQSHARE="$PREFIXCOQ/share/"
# fi
- # mkdir -p "$PREFIXCOQ/ide"
- # mv "$COQSHARE"*.png "$PREFIXCOQ/ide"
+ # mkdir -p "$PREFIXCOQ/ide/coqide"
+ # mv "$COQSHARE"*.png "$PREFIXCOQ/ide/coqide"
# rmdir "$PREFIXCOQ/share/coq" || true
fi
}
@@ -1598,7 +1598,7 @@ function make_coq_installer {
cp ../patches/ReplaceInFile.nsh dev/nsis
VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r')
cd dev/nsis
- logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+ logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coqide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
build_post
fi
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0d2f1dfbc7..8c5696f4f9 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-05-19-V33"
+# CACHEKEY: "bionic_coq-V2020-05-24-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -13,8 +13,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
libgtksourceview-3.0-dev \
# Dependencies of stdlib and sphinx doc
texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \
- xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \
- fonts-freefont-otf \
+ python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \
# Dependencies of source-doc and coq-makefile
texlive-science tipa
diff --git a/dev/include_printers b/dev/include_printers
index d077075eeb..30529b5fd6 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -27,7 +27,6 @@
#install_printer (* id set *) ppidset;;
#install_printer (* int set *) ppintset;;
-#install_printer (* Reductionops stcak of unfolded constants *) pp_cst_stack_t;;
#install_printer (* Reductionops machine stack *) pp_stack_t;;
(*#install_printer (* hint_db *) print_hint_db;;*)
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index 06db787488..63071bba72 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -46,7 +46,6 @@ 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
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 00050a89e1..bca1eb5754 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -169,7 +169,6 @@ let pp_idpred s = pp (pr_idpred s)
let pp_cpred s = pp (pr_cpred s)
let pp_transparent_state s = pp (pr_transparent_state s)
let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
(* proof printers *)
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index c826391cac..65eab8daa3 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -106,7 +106,6 @@ val pp_cpred : Names.Cpred.t -> unit
val pp_transparent_state : TransparentState.t -> 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:36:22 +0000