diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 | ||||
| -rw-r--r-- | dev/build/windows/MakeCoq_MinGW.bat | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06217-coqdep-at-once.sh | 3 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh | 4 | ||||
| -rw-r--r-- | dev/doc/changes.md | 5 |
5 files changed, 14 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include index 1da5e3ed18..d7059fe74f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -170,7 +170,7 @@ open Eqschemes open ExplainErr open Class -open Command +open ComDefinition open Indschemes open Ind_tables open Auto_ind_decl diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index f91b301b8c..665d541761 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -345,7 +345,7 @@ IF "%COQREGTESTING%" == "Y" ( SET "EXTRAPACKAGES= " IF NOT "%APPVEYOR%" == "True" ( - SET EXTRAPACKAGES="-P wget,curl,git,gcc-core,gcc-g++,automake1.5" + SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5 ) IF "%RUNSETUP%"=="Y" ( diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh new file mode 100644 index 0000000000..68e1901f7f --- /dev/null +++ b/dev/ci/user-overlays/06217-coqdep-at-once.sh @@ -0,0 +1,3 @@ +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/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh new file mode 100644 index 0000000000..8aea7dee3a --- /dev/null +++ b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh @@ -0,0 +1,4 @@ +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/doc/changes.md b/dev/doc/changes.md index c69be4f4de..01aa6b599b 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -46,6 +46,11 @@ We changed the type of the following functions: - `Global.body_of_constant`: same as above. +- `Constrinterp.*` generally, many functions that used to take an + `evar_map ref` have been now switched to functions that will work in + a functional way. The old style of passing `evar_map`s as references + is not supported anymore. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. |