aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--.gitlab-ci.yml20
-rw-r--r--.travis.yml61
-rw-r--r--Makefile2
-rw-r--r--Makefile.build1
-rw-r--r--Makefile.common38
-rw-r--r--Makefile.vofiles40
-rw-r--r--dev/ci/README.md27
-rw-r--r--dev/ci/appveyor.sh2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rw-r--r--dev/ci/ci-common.sh8
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh4
-rwxr-xr-xdev/ci/ci-geocoq.sh4
-rwxr-xr-xdev/ci/ci-math-comp.sh11
-rwxr-xr-xdev/ci/ci-unimath.sh5
-rwxr-xr-xdev/ci/ci-vst.sh5
-rw-r--r--dev/doc/changes.md5
-rw-r--r--dev/tools/coqdev.el33
-rw-r--r--doc/sphinx/MIGRATING238
-rw-r--r--doc/sphinx/README.rst325
-rw-r--r--doc/sphinx/README.template.rst117
-rw-r--r--doc/sphinx/addendum/implicit-coercions.rst22
-rw-r--r--doc/sphinx/addendum/micromega.rst5
-rw-r--r--doc/sphinx/addendum/miscellaneous-extensions.rst2
-rwxr-xr-xdoc/sphinx/conf.py12
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst4
-rw-r--r--doc/sphinx/practical-tools/coq-commands.rst15
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst36
-rw-r--r--doc/sphinx/proof-engine/tactics.rst28
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst16
-rw-r--r--doc/tools/coqrst/coqdoc/main.py3
-rw-r--r--doc/tools/coqrst/coqdomain.py330
-rwxr-xr-xdoc/tools/coqrst/regen_readme.py58
-rw-r--r--doc/tools/coqrst/repl/coqtop.py4
-rw-r--r--kernel/byterun/coq_fix_code.c51
-rw-r--r--kernel/byterun/coq_fix_code.h2
-rw-r--r--kernel/byterun/coq_interp.c34
-rw-r--r--kernel/byterun/coq_memory.c20
-rw-r--r--kernel/byterun/coq_values.c31
-rw-r--r--kernel/cemitcodes.ml4
-rw-r--r--kernel/vmvalues.ml32
-rw-r--r--man/coqtop.12
-rw-r--r--test-suite/Makefile75
-rw-r--r--test-suite/README.md3
-rwxr-xr-xtest-suite/misc/coqc_dash_o.sh2
-rw-r--r--test-suite/output/ssr_explain_match.out55
-rw-r--r--test-suite/output/ssr_explain_match.v23
-rw-r--r--test-suite/prerequisite/ssr_mini_mathcomp.v1472
-rw-r--r--test-suite/prerequisite/ssr_ssrsyntax1.v36
-rw-r--r--test-suite/ssr/absevarprop.v96
-rw-r--r--test-suite/ssr/abstract_var2.v25
-rw-r--r--test-suite/ssr/binders.v55
-rw-r--r--test-suite/ssr/binders_of.v23
-rw-r--r--test-suite/ssr/caseview.v17
-rw-r--r--test-suite/ssr/congr.v34
-rw-r--r--test-suite/ssr/deferclear.v37
-rw-r--r--test-suite/ssr/dependent_type_err.v20
-rw-r--r--test-suite/ssr/derive_inversion.v29
-rw-r--r--test-suite/ssr/elim.v279
-rw-r--r--test-suite/ssr/elim2.v74
-rw-r--r--test-suite/ssr/elim_pattern.v27
-rw-r--r--test-suite/ssr/first_n.v21
-rw-r--r--test-suite/ssr/gen_have.v174
-rw-r--r--test-suite/ssr/gen_pattern.v33
-rw-r--r--test-suite/ssr/have_TC.v50
-rw-r--r--test-suite/ssr/have_transp.v48
-rw-r--r--test-suite/ssr/have_view_idiom.v18
-rw-r--r--test-suite/ssr/havesuff.v85
-rw-r--r--test-suite/ssr/if_isnt.v22
-rw-r--r--test-suite/ssr/intro_beta.v25
-rw-r--r--test-suite/ssr/intro_noop.v37
-rw-r--r--test-suite/ssr/ipatalternation.v18
-rw-r--r--test-suite/ssr/ltac_have.v39
-rw-r--r--test-suite/ssr/ltac_in.v26
-rw-r--r--test-suite/ssr/move_after.v19
-rw-r--r--test-suite/ssr/multiview.v58
-rw-r--r--test-suite/ssr/occarrow.v23
-rw-r--r--test-suite/ssr/patnoX.v18
-rw-r--r--test-suite/ssr/pattern.v32
-rw-r--r--test-suite/ssr/primproj.v164
-rw-r--r--test-suite/ssr/rewpatterns.v146
-rw-r--r--test-suite/ssr/set_lamda.v27
-rw-r--r--test-suite/ssr/set_pattern.v64
-rw-r--r--test-suite/ssr/ssrsyntax2.v20
-rw-r--r--test-suite/ssr/tc.v39
-rw-r--r--test-suite/ssr/typeof.v22
-rw-r--r--test-suite/ssr/unfold_Opaque.v18
-rw-r--r--test-suite/ssr/unkeyed.v31
-rw-r--r--test-suite/ssr/view_case.v31
-rw-r--r--test-suite/ssr/wlog_suff.v28
-rw-r--r--test-suite/ssr/wlogletin.v50
-rw-r--r--test-suite/ssr/wlong_intro.v20
-rw-r--r--test-suite/unit-tests/.merlin6
-rw-r--r--test-suite/unit-tests/clib/inteq.ml13
-rw-r--r--test-suite/unit-tests/clib/unicode_tests.ml15
-rw-r--r--test-suite/unit-tests/src/utest.ml74
-rw-r--r--test-suite/unit-tests/src/utest.mli12
97 files changed, 5017 insertions, 552 deletions
diff --git a/.gitignore b/.gitignore
index e2a97b3a1..f1960ba68 100644
--- a/.gitignore
+++ b/.gitignore
@@ -88,6 +88,8 @@ test-suite/coqdoc/Coqdoc.*
test-suite/coqdoc/index.html
test-suite/coqdoc/coqdoc.css
test-suite/output/MExtraction.out
+test-suite/oUnit-anon.cache
+test-suite/unit-tests/**/*.test
# documentation
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 656fd741f..c010da4cf 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,6 +1,7 @@
-image: coqci/base:V2018-05-07-V2
+image: "$IMAGE"
stages:
+ - docker
- build
- test
@@ -9,11 +10,28 @@ variables:
# Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
# for reference]
CACHEKEY: bionic_coq-V2018-05-07-V2
+ IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
# By default, jobs run in the base switch; override to select another switch
OPAM_SWITCH: "base"
# Used to select special compiler switches such as flambda, 32bits, etc...
OPAM_VARIANT: ""
+docker-boot:
+ stage: docker
+ image: docker:stable
+ services:
+ - docker:dind
+ before_script: []
+ script:
+ - docker login -u gitlab-ci-token -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
+ - cd dev/ci/docker/bionic_coq/
+ - if docker pull "$IMAGE"; then echo "Image prebuilt!"; exit 0; fi
+ - docker build -t "$IMAGE" .
+ - docker push "$IMAGE"
+ except:
+ variables:
+ - $SKIP_DOCKER == "true"
+
before_script:
- cat /proc/{cpu,mem}info || true
- ls -a # figure out if artifacts are around
diff --git a/.travis.yml b/.travis.yml
index 88eed5186..890ee6d7c 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -49,18 +49,24 @@ env:
- NATIVE_COMP="yes"
- COQ_DEST="-local"
- MAIN_TARGET="world"
- # Main test suites
- matrix:
- - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
- - TEST_TARGET="validate" TW="travis_wait"
- - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
- - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
matrix:
include:
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" EXTRA_OPAM="ounit"
+ - if: NOT (type = pull_request)
+ env:
+ - TEST_TARGET="validate" TW="travis_wait"
+ - if: NOT (type = pull_request)
+ env:
+ - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait"
+ - if: NOT (type = pull_request)
+ env:
+ - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-bignums"
- if: NOT (type = pull_request)
env:
@@ -87,39 +93,24 @@ matrix:
- TEST_TARGET="ci-equations"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-geocoq"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-fcsl-pcm"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-fiat-crypto"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-fiat-parsers"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-flocq"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-formal-topology"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-hott"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-iris-lambda-rust"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-ltac2"
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-math-classes"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-math-comp"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-mtac2"
- if: NOT (type = pull_request)
env:
@@ -127,12 +118,6 @@ matrix:
- if: NOT (type = pull_request)
env:
- TEST_TARGET="ci-sf"
- - if: NOT (type = pull_request)
- env:
- - TEST_TARGET="ci-unimath"
- - if: NOT (type = pull_request)
- env:
- - TEST_TARGET="ci-vst"
- env:
- TEST_TARGET="lint"
@@ -146,10 +131,11 @@ matrix:
- dev/lint-repository.sh
# Full Coq test-suite with two compilers
- - env:
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="test-suite"
- EXTRA_CONF="-coqide opt -with-doc yes"
- - EXTRA_OPAM="${LABLGTK}"
+ - EXTRA_OPAM="${LABLGTK} ounit"
before_install: &sphinx-install
- sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
addons:
@@ -174,13 +160,14 @@ matrix:
- python3-pip
- python3-setuptools
- - env:
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="test-suite"
- COMPILER="${COMPILER_BE}"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- EXTRA_CONF="-coqide opt -with-doc yes"
- - EXTRA_OPAM="${LABLGTK_BE}"
+ - EXTRA_OPAM="${LABLGTK_BE} ounit"
before_install: *sphinx-install
addons:
apt:
@@ -189,14 +176,15 @@ matrix:
packages: *extra-packages
# Full test-suite with flambda
- - env:
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="test-suite"
- COMPILER="${COMPILER_BE}+flambda"
- FINDLIB_VER="${FINDLIB_VER_BE}"
- CAMLP5_VER="${CAMLP5_VER_BE}"
- NATIVE_COMP="no"
- EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3"
- - EXTRA_OPAM="${LABLGTK_BE}"
+ - EXTRA_OPAM="${LABLGTK_BE} ounit"
before_install: *sphinx-install
addons:
apt:
@@ -205,7 +193,8 @@ matrix:
packages: *extra-packages
# Ocaml warnings with two compilers
- - env:
+ - if: NOT (type = pull_request)
+ env:
- MAIN_TARGET="coqocaml"
- EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- EXTRA_OPAM="${LABLGTK}"
@@ -219,7 +208,8 @@ matrix:
- libgtk2.0-dev
- libgtksourceview2.0-dev
- - env:
+ - if: NOT (type = pull_request)
+ env:
- MAIN_TARGET="coqocaml"
- COMPILER="${COMPILER_BE}"
- FINDLIB_VER="${FINDLIB_VER_BE}"
@@ -239,6 +229,7 @@ matrix:
- CAMLP5_VER=".6.17"
- NATIVE_COMP="no"
- COQ_DEST="-local"
+ - EXTRA_OPAM="ounit"
before_install:
- brew update
- brew unlink python
diff --git a/Makefile b/Makefile
index 793afb661..f914de5a6 100644
--- a/Makefile
+++ b/Makefile
@@ -58,7 +58,7 @@ FIND_SKIP_DIRS:='(' \
-name '_build_ci' -o \
-name '_install_ci' -o \
-name 'user-contrib' -o \
- -name 'coq-makefile' -o \
+ -name 'test-suite' -o \
-name '.opamcache' -o \
-name '.coq-native' \
')' -prune -o
diff --git a/Makefile.build b/Makefile.build
index ffe605757..179ca28b6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -89,6 +89,7 @@ byte: coqbyte coqide-byte pluginsbyte printers
MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml)
include Makefile.common
+include Makefile.vofiles
include Makefile.doc ## provides the 'documentation' rule
include Makefile.checker
include Makefile.ide ## provides the 'coqide' rule
diff --git a/Makefile.common b/Makefile.common
index eed41fbe7..9493acd1f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -105,16 +105,12 @@ BYTERUN:=$(addprefix kernel/byterun/, \
CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
- stm/stm.cma toplevel/toplevel.cma
+ stm/stm.cma toplevel/toplevel.cma
TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma
GRAMMARCMA:=grammar/grammar.cma
-# modules known by the toplevel of Coq
-
-OBJSMOD:=$(shell cat $(CORECMA:.cma=.mllib))
-
###########################################################################
# plugins object files
###########################################################################
@@ -163,40 +159,8 @@ PLUGINSOPT:=$(PLUGINSCMO:.cmo=.cmxs)
LINKCMO:=$(CORECMA) $(STATICPLUGINS)
LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
-###########################################################################
-# vo files
-###########################################################################
-
-THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
-PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
-ALLVO := $(THEORIESVO) $(PLUGINSVO)
-VFILES := $(ALLVO:.vo=.v)
-
-## More specific targets
-
-THEORIESLIGHTVO:= \
- $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
-
ALLSTDLIB := test-suite/misc/universes/all_stdlib
-# convert a (stdlib) filename into a module name:
-# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
-vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
-
-ALLMODS:=$(call vo_to_mod,$(ALLVO))
-
-
-# Converting a stdlib filename into native compiler filenames
-# Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
-
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
-
-GLOBFILES:=$(ALLVO:.vo=.glob)
-LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
- $(call vo_to_obj,$(ALLVO)) \
- $(VFILES) $(GLOBFILES)
-
# For emacs:
# Local Variables:
# mode: makefile
diff --git a/Makefile.vofiles b/Makefile.vofiles
new file mode 100644
index 000000000..fc902c4a8
--- /dev/null
+++ b/Makefile.vofiles
@@ -0,0 +1,40 @@
+
+# This file calls [find] and as such is not suitable for inclusion in
+# the test suite Makefile, unlike Makefile.common.
+
+###########################################################################
+# vo files
+###########################################################################
+
+THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
+ALLVO := $(THEORIESVO) $(PLUGINSVO)
+VFILES := $(ALLVO:.vo=.v)
+
+## More specific targets
+
+THEORIESLIGHTVO:= \
+ $(filter theories/Init/% theories/Logic/% theories/Unicode/% theories/Arith/%, $(THEORIESVO))
+
+# convert a (stdlib) filename into a module name:
+# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
+vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+
+ALLMODS:=$(call vo_to_mod,$(ALLVO))
+
+
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+
+GLOBFILES:=$(ALLVO:.vo=.glob)
+LIBFILES:=$(ALLVO) $(call vo_to_cm,$(ALLVO)) \
+ $(call vo_to_obj,$(ALLVO)) \
+ $(VFILES) $(GLOBFILES)
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 87f03aa99..dee3d2aff 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps:
2. Click on "New Project".
3. Choose "CI / CD for external repository" then click on "GitHub".
4. Find your fork of the Coq repository and click on "Connect".
-5. You are encouraged to go to the CI / CD general settings and increase the
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
timeout from 1h to 2h for better reliability.
Now everytime you push (including force-push unless you changed the default
@@ -137,3 +138,27 @@ Currently, available artifacts are:
As an exception to the above, jobs testing that compilation triggers
no OCaml warnings build Coq in parallel with other tests.
+
+### GitLab and Windows
+
+
+If your repository has access to runners tagged `windows`, setting the
+secret variable `WINDOWS` to `enabled` will add jobs building Windows
+versions of Coq (32bit and 64bit).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+System and opam packages are installed in a Docker image. The image is
+automatically built and uploaded to your GitLab registry, and is
+loaded by subsequent jobs.
+
+The Docker building job reuses the uploaded image if it is available,
+but if you wish to save more time you can skip the job by setting
+`SKIP_DOCKER` to `true`.
+
+This means you will need to change its value when the Docker image
+needs to be updated. You can do so for a single pipeline by starting
+it through the web interface.
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 93e7bd99a..c72705c7f 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -5,5 +5,5 @@ tar -xf opam64.tar.xz
bash opam64/install.sh
opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
eval "$(opam config env)"
-opam install -y ocamlfind camlp5
+opam install -y ocamlfind camlp5 ounit
cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b7faea13e..5c882ee85 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -11,6 +11,8 @@
########################################################################
: "${mathcomp_CI_BRANCH:=master}"
: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}"
+: "${oddorder_CI_BRANCH:=master}"
+: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}"
########################################################################
# UniMath
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2a14ed352..f867fd189 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -71,11 +71,6 @@ git_checkout()
echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
}
-checkout_mathcomp()
-{
- git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
make()
{
# +x: add x only if defined
@@ -93,7 +88,8 @@ install_ssreflect()
{
echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
- checkout_mathcomp "${mathcomp_CI_DIR}"
+ git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
( cd "${mathcomp_CI_DIR}/mathcomp" && \
sed -i.bak '/ssrtest/d' Make && \
sed -i.bak '/odd_order/d' Make && \
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 845addb4c..5d96c2499 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,6 +6,8 @@ ci_dir="$(dirname "$0")"
fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto"
git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}"
+
( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive )
-( cd "${fiat_crypto_CI_DIR}" && make lite lite-display )
+fiat_crypto_CI_TARGETS="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display"
+( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index bd1d88993..920272bcf 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
-( cd "${GeoCoq_CI_DIR}" && \
- ./configure-ci.sh && \
- make )
+( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 8c6b910bb..20328baf2 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
+oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order"
-checkout_mathcomp "${mathcomp_CI_DIR}"
+git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}"
-# odd_order takes too much time for travis.
-( cd "${mathcomp_CI_DIR}/mathcomp" && \
- sed -i.bak '/PFsection/d' Make && \
- sed -i.bak '/stripped_odd_order_theorem/d' Make && \
- make Makefile.coq && make -f Makefile.coq all )
+( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install )
+( cd "${oddorder_CI_DIR}/" && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 62a949f59..aa20fe1ff 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
-( cd "${UniMath_CI_DIR}" && \
- sed -i.bak '/Folds/d' Makefile && \
- sed -i.bak '/HomologicalAlgebra/d' Makefile && \
- make BUILD_COQ=no )
+( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 79001c547..7a097eaab 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")"
VST_CI_DIR="${CI_BUILD_DIR}/VST"
-# opam install -j ${NJOBS} -y menhir
git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
-# We have to omit progs as otherwise we timeout on Travis; on Gitlab
-# we will be able to just use `make`
-( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true )
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 6d7c0d368..fb3f751db 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -22,6 +22,11 @@ Proof engine
should indicate what the canonical form is. An important change is
the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+### Unit testing
+
+ The test suite now allows writing unit tests against OCaml code in the Coq
+ code base. Those unit tests create a dependency on the OUnit test framework.
+
## Changes between Coq 8.7 and Coq 8.8
### Bug tracker
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 9dd12087a..70a9756e5 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
;; If you load this file from a git repository, checking out an old
;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup. To ignore those errors use (require 'coqdev nil t). If you
;; check out a malicious commit Emacs startup would allow it to run
;; arbitrary code, to avoid this you can copy coqdev.el to any
;; location and adjust the load path accordingly (of course if you run
@@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'."
(setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+ "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT. BEG and END default to the bounds
+of the current region. Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+ (unless beg
+ (if (region-active-p)
+ (setq beg (region-beginning) end (region-end))
+ (setq beg (point) end nil)))
+ (save-excursion
+ (goto-char (or end beg))
+ (insert right))
+ (save-excursion
+ (goto-char beg)
+ (insert left))
+ (if (and end (not offset)) ;; Second test handles the ::`` case
+ (goto-char (+ end (length left) (length right)))
+ (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+ "Insert a Sphinx role template or quote the current region."
+ (interactive)
+ (pcase (read-char "Command [gntm:`]?")
+ (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+ (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+ (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+ (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+ (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+ (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
(provide 'coqdev)
;;; coqdev ends here
diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING
deleted file mode 100644
index fa6fe1537..000000000
--- a/doc/sphinx/MIGRATING
+++ /dev/null
@@ -1,238 +0,0 @@
-How to migrate the Coq Reference Manual to Sphinx
-=================================================
-
-# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools)
-
- * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
-
-# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/
-
- * pip3 install virtualenv
- * virtualenv coqsphinxing # you may want to use -p to specify the python version
- * source coqsphinxing/bin/activate # activate the virtual environment
-
-# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session.
-
-# Add this Elisp code to .emacs, if you're using emacs (recommended):
-
- (defun sphinx/quote-coq-refman-region (left right &optional beg end count)
- (unless beg
- (if (region-active-p)
- (setq beg (region-beginning) end (region-end))
- (setq beg (point) end nil)))
- (unless count
- (setq count 1))
- (save-excursion
- (goto-char (or end beg))
- (dotimes (_ count) (insert right)))
- (save-excursion
- (goto-char beg)
- (dotimes (_ count) (insert left)))
- (if (and end (characterp left)) ;; Second test handles the ::`` case
- (goto-char (+ (* 2 count) end))
- (goto-char (+ count beg))))
-
- (defun sphinx/coqtop (beg end)
- (interactive (list (region-beginning) (region-end)))
- (replace-regexp "^Coq < " " " nil beg end)
- (indent-rigidly beg end -3)
- (goto-char beg)
- (insert ".. coqtop:: all\n\n"))
-
- (defun sphinx/rst-coq-action ()
- (interactive)
- (pcase (read-char "Command?")
- (?g (sphinx/quote-coq-refman-region ":g:`" "`"))
- (?n (sphinx/quote-coq-refman-region ":n:`" "`"))
- (?t (sphinx/quote-coq-refman-region ":token:`" "`"))
- (?m (sphinx/quote-coq-refman-region ":math:`" "`"))
- (?: (sphinx/quote-coq-refman-region "::`" "`"))
- (?` (sphinx/quote-coq-refman-region "``" "``"))
- (?c (sphinx/coqtop (region-beginning) (region-end)))))
-
- (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action)
-
- With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text
- (this will make more sense once you've started editing the text).
-
-# Fork the Coq repo, if needed:
-
- https://github.com/coq/coq
-
-# Clone the repo to your work machine
-
-# Add Maxime Dénès's repo as a remote:
-
- git remote add sphinx https://github.com/maximedenes/coq.git
-
- (or choose a name other than "sphinx")
-
- Verify with:
-
- git remote -v
-
-# Fetch from the remote
-
- git fetch sphinx
-
-# Checkout the sphinx-doc branch
-
- git checkout sphinx-doc
-
- You should pull from the repo from time to time to keep your local copy up-to-date:
-
- git pull sphinx sphinx-doc
-
- You may want to create a new branch to do your work in.
-
-# Choose a Reference Manual chapter to work on at
-
- https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU
-
-# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility,
- is available in the directory porting/raw-rst/
-
- Elsewhere, depending on the chapter, there should be an almost-empty template file already created,
- which is in the location where the final version should go
-
-# Manually edit the .rst file, place it in the correct location
-
- There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst
-
- (N.B.: the migration is a work-in-progress, your suggestions are welcome)
-
- Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/.
- At the top of the file, after the chapter heading, add:
-
- :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html
- :Converted by: Your Name
-
- N.B.: These source and converted-by annotations should help for the migration phase. Later on,
- those annotations will be removed, and contributors will be mentioned in the Coq credits.
-
- Remove chapter numbers
-
- Replace section, subsection numbers with reference labels:
-
- .. _some-reference-label:
-
- Place the label before the section or subsection, followed by a blank line.
-
- Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted.
- Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form
- `TODO-n.n.n-mnemonic` we can fixup later. Example:
-
- :ref:`TODO-1.3.2-definitions`
-
- We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual.
-
- For the particular case of references to chapters, we can use a
-convention for the cross-reference name, so no TODO is needed.
-
- :ref:`thegallinaspecificationlanguage`
-
-That is, the chapter label is the chapter title, all in lower-case,
-with no spaces or punctuation. For chapters with subtitles marked with
-a ":", like those for Omega and Nsatz, use just the chapter part
-preceding the ":". These labels should already be in the
-placeholder .rst files for each chapter.
-
-
- You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a
- section or subsection, use the syntax
-
- :ref:`Some link text <label-name>`
-
- Yes, the angle-brackets are needed here!
-
- For bibliographic references (those in biblio.bib), use :cite:`thecitation`.
-
- Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see
- http://www.sphinx-doc.org/en/stable/markup/para.html.
-
- For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx
- script will run coqtop on those examples, and can show the output (or not).
-
- The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise.
- Use
-
- .. include:: replaces.rst
-
- to gain access to those definitions in your file (you might need a path prefix). Some especially-important
- replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them,
- so that they're rendered consistently.
-
- Similarly, there are some LaTeX macros in preamble.rst that can be useful.
-
- Conventions:
-
- - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``).
-
- - Metavariables are single-backquotes (e.g. `term`, `ident`)
-
- - Use the cmd directive for Vernacular commands, like:
-
- .. cmd:: Set Printing All.
-
- Within this directive, prefix metavariables (ident, term) with @:
-
- .. cmd:: Add Printing Let @ident.
-
- There's also the "cmdv" directive for variants of a command.
-
- - Use the "exn" and "warn" directives for errors and warnings:
-
- .. exn:: Something's not right.
- .. warn:: You shouldn't do that.
-
- - Use the "example" directive for examples
-
- - Use the "g" role for inline Gallina, like :g:`fun x => x`
-
- - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line::
-
- your code here
-
- which prints a single colon, or put the double-colon on a newline.
-
-::
-
- your other code here
-
-# Making changes to the text
-
- The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not
- to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong
- verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days
- called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed.
-
-# Build, view the manual
-
- In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file
- associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory.
- Make any changes you need until there are no build warnings and the output is perfect. :-)
-
-# Creating pull requests
-
- When your changes are done, commit them, push to your fork:
-
- git commit -m "useful commit message" file
- git push origin sphinx-doc
-
- (or push to another branch, if you've created one). Then go to your GitHub
- fork and create a pull request against Maxime's sphinx-doc
- branch. If your commit is recent, you should see a link on your
- fork's code page to do that. Otherwise, you may need to go to your
- branch on GitHub to do that.
-
-# Issues/Questions/Suggestions
-
- As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact:
-
- Paul Steckler <steck@stecksoft.com>
- Maxime Dénès <maxime.denes@inria.fr>
-
-# Issues
-
- Should the stuff in replaces.rst go in preamble.rst?
- In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that?
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
new file mode 100644
index 000000000..5f2f21f2b
--- /dev/null
+++ b/doc/sphinx/README.rst
@@ -0,0 +1,325 @@
+=============================
+ Documenting Coq with Sphinx
+=============================
+
+..
+ README.rst is auto-generated from README.template.rst and the coqrst docs;
+ use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
+
+Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
+
+In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands.
+
+Coq objects
+===========
+
+Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
+
+ .. tacv:: simpl @pattern at {+ @num}
+ :name: simpl_at
+
+ This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
+ matching :n:`@pattern` in the current goal.
+
+ .. exn:: Too few occurrences
+
+Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
+
+Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above.
+
+- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```.
+- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
+- Vernac variants, tactic notations, and tactic variants do not have a default name.
+
+Notations
+---------
+
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
+
+``@…``
+ A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
+
+``{? …}``
+ an optional block
+
+``{* …}``, ``{+ …}``
+ an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces
+
+``{*, …}``, ``{+, …}``
+ an optional or mandatory repeatable block, with repetitions separated by commas
+
+``%|``, ``%{``, …
+ an escaped character (rendered without the leading ``%``)
+
+..
+ FIXME document the new subscript support
+
+As an exercise, what do the following patterns mean?
+
+.. code::
+
+ pattern {+, @term {? at {+ @num}}}
+ generalize {+, @term at {+ @num} as @ident}
+ fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
+
+Objects
+-------
+
+Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL):
+
+``.. cmd::`` :black_nib: A Coq command.
+ Example::
+
+ .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+
+ This command is equivalent to :n:`…`.
+
+``.. cmdv::`` :black_nib: A variant of a Coq command.
+ Example::
+
+ .. cmd:: Axiom @ident : @term.
+
+ This command links :token:`term` to the name :token:`term` as its specification in
+ the global context. The fact asserted by :token:`term` is thus assumed as a
+ postulate.
+
+ .. cmdv:: Parameter @ident : @term.
+
+ This is equivalent to :n:`Axiom @ident : @term`.
+
+``.. exn::`` :black_nib: An error raised by a Coq command or tactic.
+ This commonly appears nested in the ``.. tacn::`` that raises the
+ exception.
+
+ Example::
+
+ .. tacv:: assert @form by @tactic
+
+ This tactic applies :n:`@tactic` to solve the subgoals generated by
+ ``assert``.
+
+ .. exn:: Proof is not complete
+
+ Raised if :n:`@tactic` does not fully solve the goal.
+
+``.. opt::`` :black_nib: A Coq option.
+ Example::
+
+ .. opt:: Nonrecursive Elimination Schemes
+
+ This option controls whether types declared with the keywords
+ :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+ induction principles.
+
+``.. prodn::`` :black_nib: Grammar productions.
+ This is useful if you intend to document individual grammar productions.
+ Otherwise, use Sphinx's `production lists
+ <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+
+``.. tacn::`` :black_nib: A tactic, or a tactic notation.
+ Example::
+
+ .. tacn:: do @num @expr
+
+ :token:`expr` is evaluated to ``v`` which must be a tactic value. …
+
+``.. tacv::`` :black_nib: A variant of a tactic.
+ Example::
+
+ .. tacn:: fail
+
+ This is the always-failing tactic: it does not solve any goal. It is
+ useful for defining other tacticals since it can be caught by
+ :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching
+ tacticals. …
+
+ .. tacv:: fail @natural
+
+ The number is the failure level. If no level is specified, it
+ defaults to 0. …
+
+``.. thm::`` A theorem.
+ Example::
+
+ .. thm:: Bound on the ceiling function
+
+ Let :math:`p` be an integer and :math:`c` a rational constant. Then
+ :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
+
+``.. warn::`` :black_nib: An warning raised by a Coq command or tactic..
+ Do not mistake this for ``.. warning::``; this directive is for warning
+ messages produced by Coq.
+
+
+ Example::
+
+ .. warn:: Ambiguous path
+
+ When the coercion :token:`qualid` is added to the inheritance graph, non
+ valid coercion paths are ignored.
+
+Coq directives
+==============
+
+In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives:
+
+``.. coqtop::`` A reST directive to describe interactions with Coqtop.
+ Usage::
+
+ .. coqtop:: options…
+
+ Coq code to send to coqtop
+
+ Example::
+
+ .. coqtop:: in reset undo
+
+ Print nat.
+ Definition a := 1.
+
+ Here is a list of permissible options:
+
+ - Display options
+
+ - ``all``: Display input and output
+ - ``in``: Display only input
+ - ``out``: Display only output
+ - ``none``: Display neither (useful for setup commands)
+
+ - Behavior options
+
+ - ``reset``: Send a ``Reset Initial`` command before running this block
+ - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
+ running all the commands in this block
+
+ ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+ of the same document (``coqrst`` creates a single ``coqtop`` process per
+ reST source file). Use the ``reset`` option to reset Coq's state.
+
+``.. coqdoc::`` A reST directive to display Coqtop-formatted source code.
+ Usage::
+
+ .. coqdoc::
+
+ Coq code to highlight
+
+ Example::
+
+ .. coqdoc::
+
+ Definition test := 1.
+
+``.. example::`` A reST directive for examples.
+ This behaves like a generic admonition; see
+ http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
+ for more details.
+
+ Example::
+
+ .. example:: Adding a hint to a database
+
+ The following adds ``plus_comm`` to the ``plu`` database:
+
+ .. coqdoc::
+
+ Hint Resolve plus_comm : plu.
+
+``.. inference::`` A reST directive to format inference rules.
+ This also serves as a small illustration of the way to create new Sphinx
+ directives.
+
+ Usage::
+
+ .. inference:: name
+
+ newline-separated premisses
+ ------------------------
+ conclusion
+
+ Example::
+
+ .. inference:: Prod-Pro
+
+ \WTEG{T}{s}
+ s \in \Sort
+ \WTE{\Gamma::(x:T)}{U}{\Prop}
+ -----------------------------
+ \WTEG{\forall~x:T,U}{\Prop}
+
+``.. preamble::`` A reST directive for hidden math.
+ Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s.
+
+ Example::
+
+ .. preamble::
+
+ \newcommand{\paren}[#1]{\left(#1\right)}
+
+Coq roles
+=========
+
+In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles:
+
+``:g:`` Coq code.
+ Use this for Gallina and Ltac snippets::
+
+ :g:`apply plus_comm; reflexivity`
+ :g:`Set Printing All.`
+ :g:`forall (x: t), P(x)`
+
+``:n:`` Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
+ Use this to explain tactic equivalences. For example, you might write
+ this::
+
+ :n:`generalize @term as @ident` is just like :n:`generalize @term`, but
+ it names the introduced hypothesis :token:`ident`.
+
+ Note that this example also uses ``:token:``. That's because ``ident`` is
+ defined in the the Coq manual as a grammar production, and ``:token:``
+ creates a link to that. When referring to a placeholder that happens to be
+ a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
+
+``:production:`` A grammar production not included in a ``productionlist`` directive.
+ Useful to informally introduce a production, as part of running text.
+
+ Example::
+
+ :production:`string` indicates a quoted string.
+
+ You're not likely to use this role very commonly; instead, use a
+ `production list
+ <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
+ and reference its tokens using ``:token:`…```.
+
+Tips and tricks
+===============
+
+Nested lemmas
+-------------
+
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas::
+
+ .. coqtop:: all
+
+ Lemma l1: 1 + 1 = 2.
+
+ .. coqtop:: all
+
+ Lemma l2: 2 + 2 <> 1.
+
+Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+
+Abbreviations and macros
+------------------------
+
+Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
+
+Emacs
+-----
+
+The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function.
+
+Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
+
+ (with-eval-after-load 'rst
+ (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
new file mode 100644
index 000000000..203251abf
--- /dev/null
+++ b/doc/sphinx/README.template.rst
@@ -0,0 +1,117 @@
+=============================
+ Documenting Coq with Sphinx
+=============================
+
+..
+ README.rst is auto-generated from README.template.rst and the coqrst docs;
+ use ``doc/tools/coqrst/regen_readme.py`` to rebuild it.
+
+Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_.
+
+In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands.
+
+Coq objects
+===========
+
+Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise::
+
+ .. tacv:: simpl @pattern at {+ @num}
+ :name: simpl_at
+
+ This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
+ matching :n:`@pattern` in the current goal.
+
+ .. exn:: Too few occurrences
+
+Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```.
+
+Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above.
+
+- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```.
+- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
+- Vernac variants, tactic notations, and tactic variants do not have a default name.
+
+Notations
+---------
+
+The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_):
+
+``@…``
+ A placeholder (``@ident``, ``@num``, ``@tactic``\ …)
+
+``{? …}``
+ an optional block
+
+``{* …}``, ``{+ …}``
+ an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces
+
+``{*, …}``, ``{+, …}``
+ an optional or mandatory repeatable block, with repetitions separated by commas
+
+``%|``, ``%{``, …
+ an escaped character (rendered without the leading ``%``)
+
+..
+ FIXME document the new subscript support
+
+As an exercise, what do the following patterns mean?
+
+.. code::
+
+ pattern {+, @term {? at {+ @num}}}
+ generalize {+, @term at {+ @num} as @ident}
+ fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)}
+
+Objects
+-------
+
+Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL):
+
+[OBJECTS]
+
+Coq directives
+==============
+
+In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives:
+
+[DIRECTIVES]
+
+Coq roles
+=========
+
+In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles:
+
+[ROLES]
+
+Tips and tricks
+===============
+
+Nested lemmas
+-------------
+
+The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas::
+
+ .. coqtop:: all
+
+ Lemma l1: 1 + 1 = 2.
+
+ .. coqtop:: all
+
+ Lemma l2: 2 + 2 <> 1.
+
+Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas.
+
+Abbreviations and macros
+------------------------
+
+Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_.
+
+Emacs
+-----
+
+The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function.
+
+Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``::
+
+ (with-eval-after-load 'rst
+ (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action))
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 152f4f655..09faa0676 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -140,29 +140,29 @@ Declaration of Coercions
.. warn:: Ambiguous path.
- When the coercion `qualid` is added to the inheritance graph, non
- valid coercion paths are ignored; they are signaled by a warning
- displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+ When the coercion :token:`qualid` is added to the inheritance graph, non
+ valid coercion paths are ignored; they are signaled by a warning
+ displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
.. cmdv:: Local Coercion @qualid : @class >-> @class
- Declares the construction denoted by `qualid` as a coercion local to
- the current section.
+ Declares the construction denoted by `qualid` as a coercion local to
+ the current section.
.. cmdv:: Coercion @ident := @term
- This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
- and then declares `ident` as a coercion between it source and its target.
+ This defines `ident` just like ``Definition`` `ident` ``:=`` `term`,
+ and then declares `ident` as a coercion between it source and its target.
.. cmdv:: Coercion @ident := @term : @type
- This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
- and then declares `ident` as a coercion between it source and its target.
+ This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`,
+ and then declares `ident` as a coercion between it source and its target.
.. cmdv:: Local Coercion @ident := @term
- This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
- and then declares `ident` as a coercion between it source and its target.
+ This defines `ident` just like ``Let`` `ident` ``:=`` `term`,
+ and then declares `ident` as a coercion between it source and its target.
Assumptions can be declared as coercions at declaration time.
This extends the grammar of assumptions from
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f887a5fee..0e9c23b9b 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin
.. _ceil_thm:
-**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then
+.. thm:: Bound on the ceiling function
- :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`
+ Let :math:`p` be an integer and :math:`c` a rational constant. Then
+ :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
For instance, from 2 x = 1 we can deduce
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst
index 80ea8a116..b6c35d8fa 100644
--- a/doc/sphinx/addendum/miscellaneous-extensions.rst
+++ b/doc/sphinx/addendum/miscellaneous-extensions.rst
@@ -11,7 +11,7 @@ Program derivation
|Coq| comes with an extension called ``Derive``, which supports program
derivation. Typically in the style of Bird and Meertens or derivations
of program refinements. To use the Derive extension it must first be
-required with ``Require Coq.Derive.Derive``. When the extension is loaded,
+required with ``Require Coq.derive.Derive``. When the extension is loaded,
it provides the following command:
.. cmd:: Derive @ident SuchThat @term As @ident
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 23bc9a2e4..1f7dd9d68 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -96,11 +96,13 @@ language = None
# directories to ignore when looking for source files.
# This patterns also effect to html_static_path and html_extra_path
exclude_patterns = [
- '_build',
- 'Thumbs.db',
- '.DS_Store',
- 'introduction.rst',
- 'credits.rst'
+ '_build',
+ 'Thumbs.db',
+ '.DS_Store',
+ 'introduction.rst',
+ 'credits.rst',
+ 'README.rst',
+ 'README.template.rst'
]
# The reST default role (used for this markup: `text`) to use for all
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index aa41f8058..4dcd7deb1 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -553,8 +553,8 @@ has type :token:`type`.
.. cmd:: Axiom @ident : @term
- This command links *term* to the name *ident* as its specification in
- the global context. The fact asserted by *term* is thus assumed as a
+ This command links :token:`term` to the name :token:`ident` as its specification in
+ the global context. The fact asserted by :token:`term` is thus assumed as a
postulate.
.. exn:: @ident already exists.
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 83dddab4f..ad1f0caa6 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -55,15 +55,20 @@ Customization at launch time
By resource file
~~~~~~~~~~~~~~~~~~~~~~~
-When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file
-``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME``
+When |Coq| is launched, with either ``coqtop`` or ``coqc``, the
+resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will
+be implicitly prepended to any document read by Coq, whether it is an
+interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME``
is the configuration directory of the user (by default its home
-directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If
+directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If
this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is
-searched. You can also specify an arbitrary name for the resource file
+searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched,
+and, if still not found, the file ``~/.coqrc``. If the latter is also
+absent, no resource file is loaded.
+You can also specify an arbitrary name for the resource file
(see option ``-init-file`` below).
-This file may contain, for instance, ``Add LoadPath`` commands to add
+The resource file may contain, for instance, ``Add LoadPath`` commands to add
directories to the load path of |Coq|. It is possible to skip the
loading of the resource file with the option ``-q``.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 892ddbc16..6d0b27728 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -542,23 +542,23 @@ Controlling the effect of proof editing commands
.. opt:: Hyps Limit @num
-This option controls the maximum number of hypotheses displayed in goals
-after the application of a tactic. All the hypotheses remain usable
-in the proof development.
-When unset, it goes back to the default mode which is to print all
-available hypotheses.
+ This option controls the maximum number of hypotheses displayed in goals
+ after the application of a tactic. All the hypotheses remain usable
+ in the proof development.
+ When unset, it goes back to the default mode which is to print all
+ available hypotheses.
.. opt:: Automatic Introduction
-This option controls the way binders are handled
-in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is on, which is the default, binders are automatically put in
-the local context of the goal to prove.
+ This option controls the way binders are handled
+ in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the
+ option is on, which is the default, binders are automatically put in
+ the local context of the goal to prove.
-When the option is off, binders are discharged on the statement to be
-proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
-has to be used to move the assumptions to the local context.
+ When the option is off, binders are discharged on the statement to be
+ proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
+ has to be used to move the assumptions to the local context.
Controlling memory usage
@@ -570,13 +570,13 @@ to force |Coq| to optimize some of its internal data structures.
.. cmd:: Optimize Proof
-This command forces |Coq| to shrink the data structure used to represent
-the ongoing proof.
+ This command forces |Coq| to shrink the data structure used to represent
+ the ongoing proof.
.. cmd:: Optimize Heap
-This command forces the |OCaml| runtime to perform a heap compaction.
-This is in general an expensive operation.
-See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tacn:`optimize_heap`.
+ This command forces the |OCaml| runtime to perform a heap compaction.
+ This is in general an expensive operation.
+ See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+ There is also an analogous tactic :tacn:`optimize_heap`.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 0318bddde..3835524f0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -653,7 +653,7 @@ be applied or the goal is not head-reducible.
This repeats ``intro`` until it meets the head-constant. It never
reduces head-constants and it never fails.
-.. tac:: intro @ident
+.. tacn:: intro @ident
This applies ``intro`` but forces :n:`@ident` to be the name of the
introduced hypothesis.
@@ -904,15 +904,15 @@ quantification or an implication.
.. tacn:: revert {+ @ident}
:name: revert
-This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses
-(possibly defined) to the goal, if this respects dependencies. This tactic is
-the inverse of :tacn:`intro`.
+ This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses
+ (possibly defined) to the goal, if this respects dependencies. This tactic is
+ the inverse of :tacn:`intro`.
.. exn:: No such hypothesis.
.. exn:: @ident is used in the hypothesis @ident.
-.. tac:: revert dependent @ident
+.. tacn:: revert dependent @ident
This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that
depend on it.
@@ -1122,7 +1122,7 @@ Controlling the proof flow
This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
Coq.
-.. tacv:: assert form by tactic
+.. tacv:: assert @form by @tactic
This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
generated by assert.
@@ -1130,7 +1130,7 @@ Controlling the proof flow
.. exn:: Proof is not complete.
:name: Proof is not complete. (assert)
-.. tacv:: assert form as intro_pattern
+.. tacv:: assert @form as @intro_pattern
If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
the hypothesis is named after this introduction pattern (in particular, if
@@ -1139,7 +1139,7 @@ Controlling the proof flow
introduction pattern, the tactic behaves like :n:`assert form` followed by
the action done by this introduction pattern.
-.. tacv:: assert form as intro_pattern by tactic
+.. tacv:: assert @form as @intro_pattern by @tactic
This combines the two previous variants of :n:`assert`.
@@ -1192,9 +1192,9 @@ Controlling the proof flow
This behaves like :n:`enough form` using :n:`intro_pattern` to name or
destruct the new hypothesis.
-.. tacv:: enough (@ident : form) by tactic
-.. tacv:: enough form by tactic
-.. tacv:: enough form as intro_pattern by tactic
+.. tacv:: enough (@ident : @form) by @tactic
+.. tacv:: enough @form by @tactic
+.. tacv:: enough @form as @intro_pattern by @tactic
This behaves as above but with :n:`tactic` expected to solve the initial goal
after the extra assumption :n:`form` is added and possibly destructed. If the
@@ -3240,7 +3240,9 @@ the processing of the rewriting rules.
The rewriting rule bases are built with the ``Hint Rewrite vernacular``
command.
-.. warn:: This tactic may loop if you build non terminating rewriting systems.
+.. warning::
+
+ This tactic may loop if you build non terminating rewriting systems.
.. tacv:: autorewrite with {+ @ident} using @tactic
@@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
Declares each :n:`@ident` as a transparent or opaque constant.
- .. cmdv:: Hint Extern @num {? @pattern} => tactic
+ .. cmdv:: Hint Extern @num {? @pattern} => @tactic
:name: Hint Extern
This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 682553c31..838926d65 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -106,15 +106,15 @@ Automatic declaration of schemes
.. opt:: Elimination Schemes
-It is possible to deactivate the automatic declaration of the
-induction principles when defining a new inductive type with the
-``Unset Elimination Schemes`` command. It may be reactivated at any time with
-``Set Elimination Schemes``.
+ It is possible to deactivate the automatic declaration of the
+ induction principles when defining a new inductive type with the
+ ``Unset Elimination Schemes`` command. It may be reactivated at any time with
+ ``Set Elimination Schemes``.
.. opt:: Nonrecursive Elimination Schemes
-This option controls whether types declared with the keywords :cmd:`Variant` and
-:cmd:`Record` get an automatic declaration of the induction principles.
+ This option controls whether types declared with the keywords :cmd:`Variant` and
+ :cmd:`Record` get an automatic declaration of the induction principles.
.. opt:: Case Analysis Schemes
@@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and
.. opt:: Decidable Equality Schemes
-These flags control the automatic declaration of those Boolean equalities (see
-the second variant of ``Scheme``).
+ These flags control the automatic declaration of those Boolean equalities (see
+ the second variant of ``Scheme``).
.. warning::
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py
index d464f75bb..a004959eb 100644
--- a/doc/tools/coqrst/coqdoc/main.py
+++ b/doc/tools/coqrst/coqdoc/main.py
@@ -32,8 +32,9 @@ COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals',
COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"]
COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS)
-def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")):
+def coqdoc(coq_code, coqdoc_bin=None):
"""Get the output of coqdoc on coq_code."""
+ coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc")
fd, filename = mkstemp(prefix="coqdoc-", suffix=".v")
try:
os.write(fd, COQDOC_HEADER.encode("utf-8"))
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 21093bd90..606d725bf 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -1,3 +1,4 @@
+# -*- coding: utf-8 -*-
##########################################################################
## # The Coq Proof Assistant / The Coq Development Team ##
## v # INRIA, CNRS and contributors - Copyright 1999-2018 ##
@@ -57,30 +58,37 @@ def make_target(objtype, targetid):
return "coq:{}.{}".format(objtype, targetid)
class CoqObject(ObjectDescription):
- """A generic Coq object; all Coq objects are subclasses of this.
+ """A generic Coq object for Sphinx; all Coq objects are subclasses of this.
The fields and methods to override are listed at the top of this class'
implementation. Each object supports the :name: option, which gives an
explicit name to link to.
- See the documentation of CoqDomain for high-level information.
+ See the comments and docstrings in CoqObject for more information.
"""
- # The semantic domain in which this object lives.
+ # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…).
# It matches exactly one of the roles used for cross-referencing.
- subdomain = None
+ subdomain = None # type: str
- # The suffix to use in indices for objects of this type
- index_suffix = None
+ # The suffix to use in indices for objects of this type (eg. “(tac)”)
+ index_suffix = None # type: str
# The annotation to add to headers of objects of this type
- annotation = None
+ # (eg. “Command”, “Theorem”)
+ annotation = None # type: str
def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument
"""Convert a signature into a name to link to.
+ ‘Signature’ is Sphinx parlance for an object's header (think “type
+ signature”); for example, the signature of the simplest form of the
+ ``exact`` tactic is ``exact @id``.
+
Returns None by default, in which case no name will be automatically
- generated.
+ generated. This is a convenient way to automatically generate names
+ (link targets) without having to write explicit names everywhere.
+
"""
return None
@@ -100,7 +108,7 @@ class CoqObject(ObjectDescription):
def handle_signature(self, signature, signode):
"""Prefix signature with the proper annotation, then render it using
- _render_signature.
+ ``_render_signature`` (for example, add “Command” in front of commands).
:returns: the name given to the resulting node, if any
"""
@@ -110,11 +118,6 @@ class CoqObject(ObjectDescription):
self._render_signature(signature, signode)
return self.options.get("name") or self._name_from_signature(signature)
- @property
- def _index_suffix(self):
- if self.index_suffix:
- return " " + self.index_suffix
-
def _record_name(self, name, target_id):
"""Record a name, mapping it to target_id
@@ -141,12 +144,14 @@ class CoqObject(ObjectDescription):
return targetid
def _add_index_entry(self, name, target):
- """Add name (with target) to the main index."""
- index_text = name + self._index_suffix
+ """Add `name` (pointing to `target`) to the main index."""
+ index_text = name
+ if self.index_suffix:
+ index_text += " " + self.index_suffix
self.indexnode['entries'].append(('single', index_text, target, '', None))
def add_target_and_index(self, name, _, signode):
- """Create a target and an index entry for name"""
+ """Attach a link target to `signode` and an index entry for `name`."""
if name:
target = self._add_target(signode, name)
# remove trailing . , found in commands, but not ... (ellipsis)
@@ -156,31 +161,44 @@ class CoqObject(ObjectDescription):
return target
class PlainObject(CoqObject):
- """A base class for objects whose signatures should be rendered literaly."""
+ """A base class for objects whose signatures should be rendered literally."""
def _render_signature(self, signature, signode):
signode += addnodes.desc_name(signature, signature)
class NotationObject(CoqObject):
- """A base class for objects whose signatures should be rendered as nested boxes."""
+ """A base class for objects whose signatures should be rendered as nested boxes.
+
+ Objects that inherit from this class can use the notation grammar (“{+ …}”,
+ “@…”, etc.) in their signature.
+ """
def _render_signature(self, signature, signode):
position = self.state_machine.get_source_and_line(self.lineno)
tacn_node = parse_notation(signature, *position)
signode += addnodes.desc_name(signature, '', tacn_node)
-class TacticObject(PlainObject):
- """An object to represent Coq tactics"""
- subdomain = "tac"
- index_suffix = "(tac)"
- annotation = None
-
class GallinaObject(PlainObject):
- """An object to represent Coq theorems"""
+ r"""A theorem.
+
+ Example::
+
+ .. thm:: Bound on the ceiling function
+
+ Let :math:`p` be an integer and :math:`c` a rational constant. Then
+ :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
+ """
subdomain = "thm"
index_suffix = "(thm)"
annotation = "Theorem"
class VernacObject(NotationObject):
- """An object to represent Coq commands"""
+ """A Coq command.
+
+ Example::
+
+ .. cmd:: Infix "@symbol" := @term ({+, @modifier}).
+
+ This command is equivalent to :n:`…`.
+ """
subdomain = "cmd"
index_suffix = "(cmd)"
annotation = "Command"
@@ -191,7 +209,20 @@ class VernacObject(NotationObject):
return m.group(0).strip()
class VernacVariantObject(VernacObject):
- """An object to represent variants of Coq commands"""
+ """A variant of a Coq command.
+
+ Example::
+
+ .. cmd:: Axiom @ident : @term.
+
+ This command links :token:`term` to the name :token:`term` as its specification in
+ the global context. The fact asserted by :token:`term` is thus assumed as a
+ postulate.
+
+ .. cmdv:: Parameter @ident : @term.
+
+ This is equivalent to :n:`Axiom @ident : @term`.
+ """
index_suffix = "(cmdv)"
annotation = "Variant"
@@ -199,18 +230,49 @@ class VernacVariantObject(VernacObject):
return None
class TacticNotationObject(NotationObject):
- """An object to represent Coq tactic notations"""
+ """A tactic, or a tactic notation.
+
+ Example::
+
+ .. tacn:: do @num @expr
+
+ :token:`expr` is evaluated to ``v`` which must be a tactic value. …
+ """
subdomain = "tacn"
index_suffix = "(tacn)"
annotation = None
class TacticNotationVariantObject(TacticNotationObject):
- """An object to represent variants of Coq tactic notations"""
+ """A variant of a tactic.
+
+ Example::
+
+ .. tacn:: fail
+
+ This is the always-failing tactic: it does not solve any goal. It is
+ useful for defining other tacticals since it can be caught by
+ :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching
+ tacticals. …
+
+ .. tacv:: fail @natural
+
+ The number is the failure level. If no level is specified, it
+ defaults to 0. …
+ """
index_suffix = "(tacnv)"
annotation = "Variant"
class OptionObject(NotationObject):
- """An object to represent Coq options"""
+ """A Coq option.
+
+ Example::
+
+ .. opt:: Nonrecursive Elimination Schemes
+
+ This option controls whether types declared with the keywords
+ :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+ induction principles.
+ """
subdomain = "opt"
index_suffix = "(opt)"
annotation = "Option"
@@ -219,7 +281,13 @@ class OptionObject(NotationObject):
return stringify_with_ellipses(signature)
class ProductionObject(NotationObject):
- """An object to represent grammar productions"""
+ """Grammar productions.
+
+ This is useful if you intend to document individual grammar productions.
+ Otherwise, use Sphinx's `production lists
+ <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_.
+ """
+ # FIXME (CPC): I have no idea what this does :/ Someone should add an example.
subdomain = "prodn"
index_suffix = None
annotation = None
@@ -258,7 +326,22 @@ class ProductionObject(NotationObject):
return [idx, node]
class ExceptionObject(NotationObject):
- """An object to represent Coq errors."""
+ """An error raised by a Coq command or tactic.
+
+ This commonly appears nested in the ``.. tacn::`` that raises the
+ exception.
+
+ Example::
+
+ .. tacv:: assert @form by @tactic
+
+ This tactic applies :n:`@tactic` to solve the subgoals generated by
+ ``assert``.
+
+ .. exn:: Proof is not complete
+
+ Raised if :n:`@tactic` does not fully solve the goal.
+ """
subdomain = "exn"
index_suffix = "(err)"
annotation = "Error"
@@ -269,7 +352,19 @@ class ExceptionObject(NotationObject):
return stringify_with_ellipses(signature)
class WarningObject(NotationObject):
- """An object to represent Coq warnings."""
+ """An warning raised by a Coq command or tactic..
+
+ Do not mistake this for ``.. warning::``; this directive is for warning
+ messages produced by Coq.
+
+
+ Example::
+
+ .. warn:: Ambiguous path
+
+ When the coercion :token:`qualid` is added to the inheritance graph, non
+ valid coercion paths are ignored.
+ """
subdomain = "warn"
index_suffix = "(warn)"
annotation = "Warning"
@@ -280,14 +375,33 @@ class WarningObject(NotationObject):
def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
#pylint: disable=unused-argument, dangerous-default-value
- """And inline role for notations"""
+ """Any text using the notation syntax (``@id``, ``{+, …}``, etc.).
+
+ Use this to explain tactic equivalences. For example, you might write
+ this::
+
+ :n:`generalize @term as @ident` is just like :n:`generalize @term`, but
+ it names the introduced hypothesis :token:`ident`.
+
+ Note that this example also uses ``:token:``. That's because ``ident`` is
+ defined in the the Coq manual as a grammar production, and ``:token:``
+ creates a link to that. When referring to a placeholder that happens to be
+ a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
+ """
notation = utils.unescape(text, 1)
position = inliner.reporter.get_source_and_line(lineno)
return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], []
def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
#pylint: disable=dangerous-default-value
- """And inline role for Coq source code"""
+ """Coq code.
+
+ Use this for Gallina and Ltac snippets::
+
+ :g:`apply plus_comm; reflexivity`
+ :g:`Set Printing All.`
+ :g:`forall (x: t), P(x)`
+ """
options['language'] = 'Coq'
return code_role(role, rawtext, text, lineno, inliner, options, content)
## Too heavy:
@@ -300,15 +414,14 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]):
# node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes)
# return [node], []
-# TODO pass different languages?
-LtacRole = GallinaRole = VernacRole = coq_code_role
+CoqCodeRole = coq_code_role
class CoqtopDirective(Directive):
"""A reST directive to describe interactions with Coqtop.
Usage::
- .. coqtop:: (options)+
+ .. coqtop:: options…
Coq code to send to coqtop
@@ -321,20 +434,28 @@ class CoqtopDirective(Directive):
Here is a list of permissible options:
- Display
- - ‘all’: Display input and output
- - ‘in’: Display only input
- - ‘out’: Display only output
- - ‘none’: Display neither (useful for setup commands)
- Behaviour
- - ‘reset’: Send a `Reset Initial` command before running this block
- - ‘undo’: Send an `Undo n` (n=number of sentences) command after running
- all the commands in this block
+ - Display options
+
+ - ``all``: Display input and output
+ - ``in``: Display only input
+ - ``out``: Display only output
+ - ``none``: Display neither (useful for setup commands)
+
+ - Behavior options
+
+ - ``reset``: Send a ``Reset Initial`` command before running this block
+ - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after
+ running all the commands in this block
+
+ ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks
+ of the same document (``coqrst`` creates a single ``coqtop`` process per
+ reST source file). Use the ``reset`` option to reset Coq's state.
"""
has_content = True
required_arguments = 0
optional_arguments = 1
final_argument_whitespace = True
+ directive_name = "coqtop"
def run(self):
# Uses a ‘container’ instead of a ‘literal_block’ to disable
@@ -349,12 +470,26 @@ class CoqtopDirective(Directive):
return [node]
class CoqdocDirective(Directive):
- """A reST directive to display Coqtop-formatted source code"""
+ """A reST directive to display Coqtop-formatted source code.
+
+ Usage::
+
+ .. coqdoc::
+
+ Coq code to highlight
+
+ Example::
+
+ .. coqdoc::
+
+ Definition test := 1.
+ """
# TODO implement this as a Pygments highlighter?
has_content = True
required_arguments = 0
optional_arguments = 0
final_argument_whitespace = True
+ directive_name = "coqdoc"
def run(self):
# Uses a ‘container’ instead of a ‘literal_block’ to disable
@@ -365,8 +500,24 @@ class CoqdocDirective(Directive):
return [wrapper]
class ExampleDirective(BaseAdmonition):
- """A reST directive for examples"""
+ """A reST directive for examples.
+
+ This behaves like a generic admonition; see
+ http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
+ for more details.
+
+ Example::
+
+ .. example:: Adding a hint to a database
+
+ The following adds ``plus_comm`` to the ``plu`` database:
+
+ .. coqdoc::
+
+ Hint Resolve plus_comm : plu.
+ """
node_class = nodes.admonition
+ directive_name = "example"
def run(self):
# ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
@@ -380,8 +531,17 @@ class ExampleDirective(BaseAdmonition):
class PreambleDirective(MathDirective):
r"""A reST directive for hidden math.
- Mostly useful to let MathJax know about `\def`s and `\newcommand`s
+ Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s.
+
+ Example::
+
+ .. preamble::
+
+ \newcommand{\paren}[#1]{\left(#1\right)}
"""
+
+ directive_name = "preamble"
+
def run(self):
self.options['nowrap'] = True
[node] = super().run()
@@ -389,14 +549,17 @@ class PreambleDirective(MathDirective):
return [node]
class InferenceDirective(Directive):
- r"""A small example of what directives let you do in Sphinx.
+ r"""A reST directive to format inference rules.
+
+ This also serves as a small illustration of the way to create new Sphinx
+ directives.
Usage::
.. inference:: name
- \n-separated premisses
- ----------------------
+ newline-separated premisses
+ ------------------------
conclusion
Example::
@@ -413,6 +576,7 @@ class InferenceDirective(Directive):
optional_arguments = 0
has_content = True
final_argument_whitespace = True
+ directive_name = "inference"
def make_math_node(self, latex):
node = displaymath()
@@ -613,7 +777,7 @@ class CoqSubdomainsIndex(Index):
Just as in the original manual, we want to have separate indices for each
Coq subdomain (tactics, commands, options, etc)"""
- name, localname, shortname, subdomains = None, None, None, None # Must be overwritten
+ name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten
def generate(self, docnames=None):
content = defaultdict(list)
@@ -635,7 +799,7 @@ class CoqVernacIndex(CoqSubdomainsIndex):
name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"]
class CoqTacticIndex(CoqSubdomainsIndex):
- name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"]
+ name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"]
class CoqOptionIndex(CoqSubdomainsIndex):
name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"]
@@ -665,10 +829,18 @@ class IndexXRefRole(XRefRole):
return title, target
def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
- """An inline role to declare grammar productions that are not in fact included
- in a `productionlist` directive.
+ """A grammar production not included in a ``productionlist`` directive.
- Useful to informally introduce a production, as part of running text
+ Useful to informally introduce a production, as part of running text.
+
+ Example::
+
+ :production:`string` indicates a quoted string.
+
+ You're not likely to use this role very commonly; instead, use a
+ `production list
+ <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
+ and reference its tokens using ``:token:`…```.
"""
#pylint: disable=dangerous-default-value, unused-argument
env = inliner.document.settings.env
@@ -681,6 +853,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
env.domaindata['std']['objects']['token', text] = env.docname, targetid
return [node], []
+GrammarProductionRole.role_name = "production"
+
class CoqDomain(Domain):
"""A domain to document Coq code.
@@ -703,7 +877,6 @@ class CoqDomain(Domain):
# ObjType (= directive type) → (Local name, *xref-roles)
'cmd': ObjType('cmd', 'cmd'),
'cmdv': ObjType('cmdv', 'cmd'),
- 'tac': ObjType('tac', 'tac'),
'tacn': ObjType('tacn', 'tacn'),
'tacv': ObjType('tacv', 'tacn'),
'opt': ObjType('opt', 'opt'),
@@ -720,7 +893,6 @@ class CoqDomain(Domain):
# the same role.
'cmd': VernacObject,
'cmdv': VernacVariantObject,
- 'tac': TacticObject,
'tacn': TacticNotationObject,
'tacv': TacticNotationVariantObject,
'opt': OptionObject,
@@ -733,7 +905,6 @@ class CoqDomain(Domain):
roles = {
# Each of these roles lives in a different semantic “subdomain”
'cmd': XRefRole(warn_dangling=True),
- 'tac': XRefRole(warn_dangling=True),
'tacn': XRefRole(warn_dangling=True),
'opt': XRefRole(warn_dangling=True),
'thm': XRefRole(warn_dangling=True),
@@ -743,12 +914,8 @@ class CoqDomain(Domain):
# This one is special
'index': IndexXRefRole(),
# These are used for highlighting
- 'notation': NotationRole,
- 'gallina': GallinaRole,
- 'ltac': LtacRole,
'n': NotationRole,
- 'g': GallinaRole,
- 'l': LtacRole, #FIXME unused?
+ 'g': CoqCodeRole
}
indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex]
@@ -759,7 +926,6 @@ class CoqDomain(Domain):
# others, such as “version”
'objects' : { # subdomain → name → docname, objtype, targetid
'cmd': {},
- 'tac': {},
'tacn': {},
'opt': {},
'thm': {},
@@ -829,11 +995,18 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint:
for node in doctree.traverse(is_coqtop_or_coqdoc_block):
if is_html:
node.rawsource = '' # Prevent pygments from kicking in
+ elif 'coqtop-hidden' in node['classes']:
+ node.parent.remove(node)
else:
- if 'coqtop-hidden' in node['classes']:
- node.parent.remove(node)
- else:
- node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
+ node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq"))
+
+COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective,
+ CoqdocDirective,
+ ExampleDirective,
+ InferenceDirective,
+ PreambleDirective]
+
+COQ_ADDITIONAL_ROLES = [GrammarProductionRole]
def setup(app):
"""Register the Coq domain"""
@@ -845,12 +1018,13 @@ def setup(app):
# Add domain, directives, and roles
app.add_domain(CoqDomain)
- app.add_role("production", GrammarProductionRole)
- app.add_directive("coqtop", CoqtopDirective)
- app.add_directive("coqdoc", CoqdocDirective)
- app.add_directive("example", ExampleDirective)
- app.add_directive("inference", InferenceDirective)
- app.add_directive("preamble", PreambleDirective)
+
+ for role in COQ_ADDITIONAL_ROLES:
+ app.add_role(role.role_name, role)
+
+ for directive in COQ_ADDITIONAL_DIRECTIVES:
+ app.add_directive(directive.directive_name, directive)
+
app.add_transform(CoqtopBlocksTransform)
app.connect('doctree-resolved', simplify_source_code_blocks_for_latex)
diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py
new file mode 100755
index 000000000..e56882a52
--- /dev/null
+++ b/doc/tools/coqrst/regen_readme.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+"""Rebuild sphinx/README.rst from sphinx/README.template.rst."""
+
+import re
+from os import sys, path
+
+SCRIPT_DIR = path.dirname(path.abspath(__file__))
+if __name__ == "__main__" and __package__ is None:
+ sys.path.append(path.dirname(SCRIPT_DIR))
+
+import sphinx
+from coqrst import coqdomain
+
+README_ROLES_MARKER = "[ROLES]"
+README_OBJECTS_MARKER = "[OBJECTS]"
+README_DIRECTIVES_MARKER = "[DIRECTIVES]"
+
+FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n")
+def format_docstring(template, obj, *strs):
+ docstring = obj.__doc__.strip()
+ strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),)
+ return template.format(*strs)
+
+SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/")
+README_PATH = path.join(SPHINX_DIR, "README.rst")
+README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst")
+
+def notation_symbol(d):
+ return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else ""
+
+def regen_readme():
+ objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj))
+ for objname, obj in sorted(coqdomain.CoqDomain.directives.items())]
+
+ roles = ([(name, cls)
+ for name, cls in sorted(coqdomain.CoqDomain.roles.items())
+ if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] +
+ [(fn.role_name, fn)
+ for fn in coqdomain.COQ_ADDITIONAL_ROLES])
+ roles_docs = [format_docstring("``:{}:`` {}", role, name)
+ for (name, role) in roles]
+
+ directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name)
+ for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES]
+
+ with open(README_TEMPLATE_PATH, encoding="utf-8") as readme:
+ contents = readme.read()
+
+ with open(README_PATH, mode="w", encoding="utf-8") as readme:
+ readme.write(contents
+ .replace(README_ROLES_MARKER, "\n\n".join(roles_docs))
+ .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs))
+ .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs)))
+
+if __name__ == '__main__':
+ regen_readme()
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index efb5cb550..aeadce4c4 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,7 +41,9 @@ class CoqTop:
the ansicolors module)
:param args: Additional arugments to coqtop.
"""
- self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop")
+ self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop")
+ if not pexpect.utils.which(self.coqtop_bin):
+ raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin))
self.args = (args or []) + ["-boot", "-color", "on"] * color
self.coqtop = None
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index d5feafbf9..be2b05da8 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -18,6 +18,7 @@
#include <caml/misc.h>
#include <caml/mlvalues.h>
#include <caml/fail.h>
+#include <caml/alloc.h>
#include <caml/memory.h>
#include "coq_instruct.h"
#include "coq_fix_code.h"
@@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz)
}
value coq_makeaccu (value i) {
- code_t q;
- code_t res = coq_stat_alloc(2 * sizeof(opcode_t));
- q = res;
+ CAMLparam1(i);
+ CAMLlocal1(res);
+ code_t q = coq_stat_alloc(2 * sizeof(opcode_t));
+ res = caml_alloc_small(1, Abstract_tag);
+ Code_val(res) = q;
*q++ = VALINSTR(MAKEACCU);
*q = (opcode_t)Int_val(i);
- return (value)res;
+ CAMLreturn(res);
}
value coq_pushpop (value i) {
- code_t res;
- int n;
- n = Int_val(i);
+ CAMLparam1(i);
+ CAMLlocal1(res);
+ code_t q;
+ res = caml_alloc_small(1, Abstract_tag);
+ int n = Int_val(i);
if (n == 0) {
- res = coq_stat_alloc(sizeof(opcode_t));
- *res = VALINSTR(STOP);
- return (value)res;
+ q = coq_stat_alloc(sizeof(opcode_t));
+ Code_val(res) = q;
+ *q = VALINSTR(STOP);
+ CAMLreturn(res);
}
else {
- code_t q;
- res = coq_stat_alloc(3 * sizeof(opcode_t));
- q = res;
+ q = coq_stat_alloc(3 * sizeof(opcode_t));
+ Code_val(res) = q;
*q++ = VALINSTR(POP);
*q++ = (opcode_t)n;
*q = VALINSTR(STOP);
- return (value)res;
+ CAMLreturn(res);
}
}
value coq_is_accumulate_code(value code){
- code_t q;
+ code_t q = Code_val(code);
int res;
- q = (code_t)code;
res = Is_instruction(q,ACCUMULATE);
return Val_bool(res);
}
@@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){
#define COPY32(dst,src) (*dst=*src)
#endif /* ARCH_BIG_ENDIAN */
-value coq_tcode_of_code (value code, value size) {
- code_t p, q, res;
- asize_t len = (asize_t) Long_val(size);
- res = coq_stat_alloc(len);
- q = res;
+value coq_tcode_of_code (value code) {
+ CAMLparam1 (code);
+ CAMLlocal1 (res);
+ code_t p, q;
+ asize_t len = (asize_t) caml_string_length(code);
+ res = caml_alloc_small(1, Abstract_tag);
+ q = coq_stat_alloc(len);
+ Code_val(res) = q;
len /= sizeof(opcode_t);
for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
opcode_t instr;
@@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) {
for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
}
}
- return (value)res;
+ CAMLreturn(res);
}
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 5c85389dd..638d6b5ab 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -26,7 +26,7 @@ void init_arity();
#define Is_instruction(pc,instr) (*pc == VALINSTR(instr))
-value coq_tcode_of_code(value code, value len);
+value coq_tcode_of_code(value code);
value coq_makeaccu (value i);
value coq_pushpop (value i);
value coq_is_accumulate_code(value code);
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index cfeb0a9ee..8ac1ecc79 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -16,6 +16,7 @@
#include <stdio.h>
#include <signal.h>
#include <stdint.h>
+#include <caml/memory.h>
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
@@ -629,7 +630,7 @@ value coq_interprete
print_instr("CLOSUREREC");
if (nvars > 0) *--sp = accu;
/* construction du vecteur de type */
- Alloc_small(accu, nfuncs, 0);
+ Alloc_small(accu, nfuncs, Abstract_tag);
for(i = 0; i < nfuncs; i++) {
Field(accu,i) = (value)(pc+pc[i]);
}
@@ -665,7 +666,7 @@ value coq_interprete
print_instr("CLOSURECOFIX");
if (nvars > 0) *--sp = accu;
/* construction du vecteur de type */
- Alloc_small(accu, nfunc, 0);
+ Alloc_small(accu, nfunc, Abstract_tag);
for(i = 0; i < nfunc; i++) {
Field(accu,i) = (value)(pc+pc[i]);
}
@@ -1071,12 +1072,22 @@ value coq_interprete
}
}
*--sp = accu;
- /* We create the switch zipper */
- Alloc_small(accu, 5, Default_tag);
- Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl;
- Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0];
- Field(accu, 4) = coq_env;
- sp++;sp[0] = accu;
+ /* Create bytecode wrappers */
+ Alloc_small(accu, 1, Abstract_tag);
+ Code_val(accu) = typlbl;
+ *--sp = accu;
+ Alloc_small(accu, 1, Abstract_tag);
+ Code_val(accu) = swlbl;
+ *--sp = accu;
+ /* We create the switch zipper */
+ Alloc_small(accu, 5, Default_tag);
+ Field(accu, 0) = sp[1];
+ Field(accu, 1) = sp[0];
+ Field(accu, 2) = sp[3];
+ Field(accu, 3) = sp[2];
+ Field(accu, 4) = coq_env;
+ sp += 3;
+ sp[0] = accu;
/* We create the atom */
Alloc_small(accu, 2, ATOM_SWITCH_TAG);
Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
@@ -1476,7 +1487,8 @@ value coq_interprete
#endif
}
-value coq_push_ra(value tcode) {
+value coq_push_ra(value code) {
+ code_t tcode = Code_val(code);
print_instr("push_ra");
coq_sp -= 3;
coq_sp[0] = (value) tcode;
@@ -1516,8 +1528,10 @@ value coq_push_vstack(value stk, value max_stack_size) {
}
value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) {
+ // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete
+ CAMLparam1(tcode);
print_instr("coq_interprete");
- return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea));
+ CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea)));
print_instr("end coq_interprete");
}
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index b2917a55e..542a05fd2 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -10,6 +10,8 @@
#include <stdio.h>
#include <string.h>
+#include <caml/alloc.h>
+#include <caml/address_class.h>
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
@@ -46,7 +48,11 @@ value coq_static_alloc(value size) /* ML */
value accumulate_code(value unit) /* ML */
{
- return (value) accumulate;
+ CAMLparam1(unit);
+ CAMLlocal1(res);
+ res = caml_alloc_small(1, Abstract_tag);
+ Code_val(res) = accumulate;
+ CAMLreturn(res);
}
static void (*coq_prev_scan_roots_hook) (scanning_action);
@@ -56,6 +62,10 @@ static void coq_scan_roots(scanning_action action)
register value * i;
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
+#ifdef NO_NAKED_POINTERS
+ /* The VM stack may contain C-allocated bytecode */
+ if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue;
+#endif
(*action) (*i, i);
};
/* Hook */
@@ -94,8 +104,12 @@ value init_coq_vm(value unit) /* ML */
/* Initialing the interpreter */
init_coq_interpreter();
- /* Some predefined pointer code */
- accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
+ /* Some predefined pointer code.
+ * It is typically contained in accumlator blocks whose tag is 0 and thus
+ * scanned by the GC, so make it look like an OCaml block. */
+ value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
+ Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \
+ accumulate = (code_t) Val_hp(accu_block);
*accumulate = VALINSTR(ACCUMULATE);
/* Initialize GC */
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 528babebf..e05f3fb82 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -9,6 +9,7 @@
/***********************************************************************/
#include <stdio.h>
+#include <caml/memory.h>
#include "coq_fix_code.h"
#include "coq_instruct.h"
#include "coq_memory.h"
@@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){
return (value)&Field(v, Int_val(offset));
}
+value coq_set_bytecode_field(value v, value i, value code) {
+ // No write barrier because the bytecode does not live on the OCaml heap
+ Field(v, Long_val(i)) = (value) Code_val(code);
+ return Val_unit;
+}
+
value coq_offset_tcode(value code,value offset){
- return((value)((code_t)code + Int_val(offset)));
+ CAMLparam1(code);
+ CAMLlocal1(res);
+ res = caml_alloc_small(1, Abstract_tag);
+ Code_val(res) = Code_val(code) + Int_val(offset);
+ CAMLreturn(res);
}
-value coq_int_tcode(value code, value offset) {
+value coq_int_tcode(value pc, value offset) {
+ code_t code = Code_val(pc);
return Val_int(*((code_t) code + Int_val(offset)));
}
+
+value coq_tcode_array(value tcodes) {
+ CAMLparam1(tcodes);
+ CAMLlocal2(res, tmp);
+ int i;
+ /* Assumes that the vector of types is small. This was implicit in the
+ previous code which was building the type array using Alloc_small. */
+ res = caml_alloc_small(Wosize_val(tcodes), Default_tag);
+ for (i = 0; i < Wosize_val(tcodes); i++) {
+ tmp = caml_alloc_small(1, Abstract_tag);
+ Code_val(tmp) = (code_t) Field(tcodes, i);
+ Store_field(res, i, tmp);
+ }
+ CAMLreturn(res);
+}
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 14f4f27c0..cea09c510 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -20,7 +20,7 @@ open Mod_subst
type emitcodes = String.t
-external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code"
(* Relocation information *)
type reloc_info =
@@ -82,7 +82,7 @@ let patch buff pl f =
(** Order seems important here? *)
let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
let buff = patch_int buff reloc in
- tcode_of_code buff (Bytes.length buff)
+ tcode_of_code buff
(* Buffering of bytecode *)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 6a41efac2..7a703e653 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -59,14 +59,17 @@ let vm_global (v : values array) = (Obj.magic v : vm_global)
(*******************************************)
type tcode
+(** A block whose first field is a C-allocated VM bytecode, encoded as char*.
+ This is compatible with the representation of the Coq VM closures. *)
+
+type tcode_array
external mkAccuCode : int -> tcode = "coq_makeaccu"
external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
-let tcode_of_obj v = ((Obj.obj v):tcode)
-let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0)
-let fix_code v = fun_code v
-let cofix_upd_code v = fun_code v
+let fun_code v = (Obj.magic v : tcode)
+let fix_code = fun_code
+let cofix_upd_code = fun_code
type vswitch = {
@@ -255,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
external int_tcode : tcode -> int -> int = "coq_int_tcode"
external accumulate : unit -> tcode = "accumulate_code"
+external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
let accumulate = accumulate ()
let whd_val : values -> whd =
@@ -284,7 +288,7 @@ let whd_val : values -> whd =
let obj_of_atom : atom -> Obj.t =
fun a ->
let res = Obj.new_block accu_tag 2 in
- Obj.set_field res 0 (Obj.repr accumulate);
+ set_bytecode_field res 0 accumulate;
Obj.set_field res 1 (Obj.repr a);
res
@@ -370,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity"
external offset : Obj.t -> int = "coq_offset"
external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+external tcode_array : tcode_array -> tcode array = "coq_tcode_array"
let first o = (offset_closure o (offset o))
let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix)
let last o = (Obj.field o (Obj.size o - 1))
-let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array)
-let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array)
+let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
+let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
let current_fix vf = - (offset (Obj.repr vf) / 2)
-let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
+let unsafe_fb_code fb i =
+ let off = (2 * i) * (Sys.word_size / 8) in
+ Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off))
let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
@@ -442,13 +449,12 @@ let relaccu_code i =
let mk_fix_body k ndef fb =
let e = Obj.dup (Obj.repr fb) in
for i = 0 to ndef - 1 do
- Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
+ set_bytecode_field e (2 * i) (relaccu_code (k + i))
done;
let fix_body i =
- let jump_grabrec c = offset_tcode c 2 in
- let c = jump_grabrec (unsafe_fb_code fb i) in
+ let c = offset_tcode (unsafe_fb_code fb i) 2 in
let res = Obj.new_block Obj.closure_tag 2 in
- Obj.set_field res 0 (Obj.repr c);
+ set_bytecode_field res 0 c;
Obj.set_field res 1 (offset_closure e (2*i));
((Obj.obj res) : vfun) in
Array.init ndef fix_body
@@ -486,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf =
Obj.set_field e 0 c;
let atom = Obj.new_block cofix_tag 1 in
let self = Obj.new_block accu_tag 2 in
- Obj.set_field self 0 (Obj.repr accumulate);
+ set_bytecode_field self 0 accumulate;
Obj.set_field self 1 (Obj.repr atom);
apply_varray (Obj.obj e) [|Obj.obj self|] in
Array.init ndef cofix_body
diff --git a/man/coqtop.1 b/man/coqtop.1
index b1fbb3262..084adfe45 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -110,7 +110,7 @@ print Coq version and exit
.TP
.B \-q
-skip loading of rcfile
+skip loading of rcfile (resource file) if any
.TP
.BI \-init\-file \ filename
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 9d84cd5c7..ce21ff41c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -8,9 +8,6 @@
## # (see LICENSE file for the text of the license) ##
##########################################################################
-# This is a standalone Makefile to run the test-suite. It can be used
-# outside of the Coq source tree (if BIN is overridden).
-
# There is one %.v.log target per %.v test file. The target will be
# filled with the output, timings and status of the test. There is
# also one target per directory containing %.v files, that runs all
@@ -23,6 +20,14 @@
# The "run" target runs all tests that have not been run yet. To force
# all tests to be run, use the "clean" target.
+
+###########################################################################
+# Includes
+###########################################################################
+
+include ../config/Makefile
+include ../Makefile.common
+
#######################################################################
# Variables
#######################################################################
@@ -94,10 +99,10 @@ INTERACTIVE := interactive
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
- coqdoc
+ coqdoc ssr
# All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-tests
PREREQUISITELOG = prerequisite/admit.v.log \
prerequisite/make_local.v.log prerequisite/make_notation.v.log \
@@ -118,13 +123,16 @@ bugs: $(BUGS)
clean:
rm -f trace .lia.cache output/MExtraction.out
- $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>"
+ $(SHOW) 'RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
$(HIDE)find . \( \
- -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
- \) -print0 | xargs -0 rm -f
-
+ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
+ \) -print0 | xargs -0 rm -f
+ $(SHOW) 'RM <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>'
+ $(HIDE)find unit-tests \( \
+ -name '*.cmx' -o -name '*.cmi' -o -name '*.o' -o -name '*.test' \
+ \) -print0 | xargs -0 rm -f
distclean: clean
- $(SHOW) "RM <**/*.aux>"
+ $(SHOW) 'RM <**/*.aux>'
$(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f
#######################################################################
@@ -158,18 +166,20 @@ summary:
$(call summary_dir, "Complexity tests", complexity); \
$(call summary_dir, "Module tests", modules); \
$(call summary_dir, "STM tests", stm); \
+ $(call summary_dir, "SSR tests", ssr); \
$(call summary_dir, "IDE tests", ide); \
$(call summary_dir, "VI tests", vio); \
$(call summary_dir, "Coqchk tests", coqchk); \
$(call summary_dir, "Coqwc tests", coqwc); \
$(call summary_dir, "Coq makefile", coq-makefile); \
$(call summary_dir, "Coqdoc tests", coqdoc); \
+ $(call summary_dir, "Unit tests", unit-tests); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
nb_tests=`expr $$nb_success + $$nb_failure`; \
- pourcentage=`expr 100 \* $$nb_success / $$nb_tests`; \
+ percentage=`expr 100 \* $$nb_success / $$nb_tests`; \
echo; \
- echo "$$nb_success tests passed over $$nb_tests, i.e. $$pourcentage %"; \
+ echo "$$nb_success tests passed over $$nb_tests, i.e. $$percentage %"; \
}
summary.log:
@@ -243,6 +253,44 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
} > "$@"
#######################################################################
+# Unit tests
+#######################################################################
+
+OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
+SYSMOD:=-package num,str,unix,dynlink,threads
+
+COQSRCDIRS:=$(addprefix -I $(LIB)/,$(CORESRCDIRS))
+COQCMXS:=$(addprefix $(LIB)/,$(LINKCMX))
+
+# ML files from unit-test framework, not containing tests
+UNIT_SRCFILES:=$(shell find ./unit-tests/src -name *.ml)
+UNIT_ALLMLFILES:=$(shell find ./unit-tests -name *.ml)
+UNIT_MLFILES:=$(filter-out $(UNIT_SRCFILES),$(UNIT_ALLMLFILES))
+UNIT_LOGFILES:=$(patsubst %.ml,%.ml.log,$(UNIT_MLFILES))
+
+UNIT_CMXS=utest.cmx
+
+unit-tests/src/utest.cmx: unit-tests/src/utest.ml unit-tests/src/utest.cmi
+ $(SHOW) 'OCAMLOPT $<'
+ $(HIDE)$(OCAMLOPT) -c -I unit-tests/src -package oUnit $<
+unit-tests/src/utest.cmi: unit-tests/src/utest.mli
+ $(SHOW) 'OCAMLOPT $<'
+ $(HIDE)$(OCAMLOPT) -package oUnit $<
+
+$(UNIT_LOGFILES): unit-tests/src/utest.cmx
+
+unit-tests: $(UNIT_LOGFILES)
+
+# Build executable, run it to generate log file
+unit-tests/%.ml.log: unit-tests/%.ml
+ $(SHOW) 'TEST $<'
+ $(HIDE)$(OCAMLOPT) -linkall -linkpkg -cclib -lcoqrun \
+ $(SYSMOD) -package camlp5.gramlib,oUnit \
+ -I unit-tests/src $(COQSRCDIRS) $(COQCMXS) \
+ $(UNIT_CMXS) $< -o $<.test;
+ $(HIDE)./$<.test
+
+#######################################################################
# Other generic tests
#######################################################################
@@ -261,7 +309,8 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
fi; \
} > "$@"
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+ssr: $(wildcard ssr/*.v:%.v=%.v.log)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
diff --git a/test-suite/README.md b/test-suite/README.md
index 1d1195646..4572c98cf 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -73,3 +73,6 @@ When you fix a bug, you should usually add a regression test here as well.
The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
+
+There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
+unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them.
diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh
index f303214b9..0ae7873fd 100755
--- a/test-suite/misc/coqc_dash_o.sh
+++ b/test-suite/misc/coqc_dash_o.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
DOUT=misc/tmp_coqc_dash_o/
OUT=${DOUT}coqc_dash_o.vo
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
new file mode 100644
index 000000000..fa2393b91
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.out
@@ -0,0 +1,55 @@
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ - _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ >= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ > _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ + _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ * _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+BEGIN INSTANCES
+instance: (x + y + z) matches: (x + y + z)
+instance: (x + y) matches: (x + y)
+instance: (x + y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnC (x + y) z) matches: (x + y + z)
+instance: (addnC x y) matches: (x + y)
+instance: (addnC x y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+instance: (addnC z (x + y)) matches: (x + y + z)
+instance: (addnC y x) matches: (x + y)
+instance: (addnC y x) matches: (x + y)
+END INSTANCES
+The command has indeed failed with message:
+Ltac call to "ssrinstancesoftpat (cpattern)" failed.
+Not supported
diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v
new file mode 100644
index 000000000..56ca24b6e
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssrmatching.
+Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp.
+
+Definition addnAC := (addnA, addnC).
+
+Lemma test x y z : x + y + z = x + y.
+
+ssrinstancesoftpat (_ + _).
+ssrinstancesofruleL2R addnC.
+ssrinstancesofruleR2L addnA.
+ssrinstancesofruleR2L addnAC.
+Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
+Admitted.
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
new file mode 100644
index 000000000..cb2c56736
--- /dev/null
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -0,0 +1,1472 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* Some code from mathcomp needed in order to run ssr_* tests *)
+
+Require Import ssreflect ssrfun ssrbool.
+
+Global Set SsrOldRewriteGoalsOrder.
+Global Set Asymmetric Patterns.
+Global Set Bullet Behavior "None".
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+(* eqtype ---------------------------------------------------------- *)
+
+Module Equality.
+
+Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
+
+Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
+Notation class_of := mixin_of (only parsing).
+
+Section ClassDef.
+
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Local Coercion sort : type >-> Sortclass.
+Variables (T : Type) (cT : type).
+
+Definition class := let: Pack _ c _ := cT return class_of cT in c.
+
+Definition pack c := @Pack T c T.
+Definition clone := fun c & cT -> T & phant_id (pack c) cT => pack c.
+
+End ClassDef.
+
+Module Exports.
+Coercion sort : type >-> Sortclass.
+Notation eqType := type.
+Notation EqMixin := Mixin.
+Notation EqType T m := (@pack T m).
+Notation "[ 'eqMixin' 'of' T ]" := (class _ : mixin_of T)
+ (at level 0, format "[ 'eqMixin' 'of' T ]") : form_scope.
+Notation "[ 'eqType' 'of' T 'for' C ]" := (@clone T C _ idfun id)
+ (at level 0, format "[ 'eqType' 'of' T 'for' C ]") : form_scope.
+Notation "[ 'eqType' 'of' T ]" := (@clone T _ _ id id)
+ (at level 0, format "[ 'eqType' 'of' T ]") : form_scope.
+End Exports.
+
+End Equality.
+Export Equality.Exports.
+
+Definition eq_op T := Equality.op (Equality.class T).
+
+Lemma eqE T x : eq_op x = Equality.op (Equality.class T) x.
+Proof. by []. Qed.
+
+Lemma eqP T : Equality.axiom (@eq_op T).
+Proof. by case: T => ? []. Qed.
+Arguments eqP [T x y].
+
+Delimit Scope eq_scope with EQ.
+Open Scope eq_scope.
+
+Notation "x == y" := (eq_op x y)
+ (at level 70, no associativity) : bool_scope.
+Notation "x == y :> T" := ((x : T) == (y : T))
+ (at level 70, y at next level) : bool_scope.
+Notation "x != y" := (~~ (x == y))
+ (at level 70, no associativity) : bool_scope.
+Notation "x != y :> T" := (~~ (x == y :> T))
+ (at level 70, y at next level) : bool_scope.
+Notation "x =P y" := (eqP : reflect (x = y) (x == y))
+ (at level 70, no associativity) : eq_scope.
+Notation "x =P y :> T" := (eqP : reflect (x = y :> T) (x == y :> T))
+ (at level 70, y at next level, no associativity) : eq_scope.
+
+Prenex Implicits eq_op eqP.
+
+Lemma eq_refl (T : eqType) (x : T) : x == x. Proof. exact/eqP. Qed.
+Notation eqxx := eq_refl.
+
+Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x).
+Proof. exact/eqP/eqP. Qed.
+
+Hint Resolve eq_refl eq_sym.
+
+
+Definition eqb b := addb (~~ b).
+
+Lemma eqbP : Equality.axiom eqb.
+Proof. by do 2!case; constructor. Qed.
+
+Canonical bool_eqMixin := EqMixin eqbP.
+Canonical bool_eqType := Eval hnf in EqType bool bool_eqMixin.
+
+Section ProdEqType.
+
+Variable T1 T2 : eqType.
+
+Definition pair_eq := [rel u v : T1 * T2 | (u.1 == v.1) && (u.2 == v.2)].
+
+Lemma pair_eqP : Equality.axiom pair_eq.
+Proof.
+move=> [x1 x2] [y1 y2] /=; apply: (iffP andP) => [[]|[<- <-]] //=.
+by do 2!move/eqP->.
+Qed.
+
+Definition prod_eqMixin := EqMixin pair_eqP.
+Canonical prod_eqType := Eval hnf in EqType (T1 * T2) prod_eqMixin.
+
+End ProdEqType.
+
+Section OptionEqType.
+
+Variable T : eqType.
+
+Definition opt_eq (u v : option T) : bool :=
+ oapp (fun x => oapp (eq_op x) false v) (~~ v) u.
+
+Lemma opt_eqP : Equality.axiom opt_eq.
+Proof.
+case=> [x|] [y|] /=; by [constructor | apply: (iffP eqP) => [|[]] ->].
+Qed.
+
+Canonical option_eqMixin := EqMixin opt_eqP.
+Canonical option_eqType := Eval hnf in EqType (option T) option_eqMixin.
+
+End OptionEqType.
+
+Notation xpred1 := (fun a1 x => x == a1).
+Notation xpredU1 := (fun a1 (p : pred _) x => (x == a1) || p x).
+
+Section EqPred.
+
+Variable T : eqType.
+
+Definition pred1 (a1 : T) := SimplPred (xpred1 a1).
+Definition predU1 (a1 : T) p := SimplPred (xpredU1 a1 p).
+
+End EqPred.
+
+Section TransferEqType.
+
+Variables (T : Type) (eT : eqType) (f : T -> eT).
+
+Lemma inj_eqAxiom : injective f -> Equality.axiom (fun x y => f x == f y).
+Proof. by move=> f_inj x y; apply: (iffP eqP) => [|-> //]; apply: f_inj. Qed.
+
+Definition InjEqMixin f_inj := EqMixin (inj_eqAxiom f_inj).
+
+Definition PcanEqMixin g (fK : pcancel f g) := InjEqMixin (pcan_inj fK).
+
+Definition CanEqMixin g (fK : cancel f g) := InjEqMixin (can_inj fK).
+
+End TransferEqType.
+
+(* We use the module system to circumvent a silly limitation that *)
+(* forbids using the same constant to coerce to different targets. *)
+Module Type EqTypePredSig.
+Parameter sort : eqType -> predArgType.
+End EqTypePredSig.
+Module MakeEqTypePred (eqmod : EqTypePredSig).
+Coercion eqmod.sort : eqType >-> predArgType.
+End MakeEqTypePred.
+Module Export EqTypePred := MakeEqTypePred Equality.
+
+
+Section SubType.
+
+Variables (T : Type) (P : pred T).
+
+Structure subType : Type := SubType {
+ sub_sort :> Type;
+ val : sub_sort -> T;
+ Sub : forall x, P x -> sub_sort;
+ _ : forall K (_ : forall x Px, K (@Sub x Px)) u, K u;
+ _ : forall x Px, val (@Sub x Px) = x
+}.
+
+Arguments Sub [s].
+Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed.
+Definition vrefl_rect := vrefl.
+
+Definition clone_subType U v :=
+ fun sT & sub_sort sT -> U =>
+ fun c Urec cK (sT' := @SubType U v c Urec cK) & phant_id sT' sT => sT'.
+
+Variable sT : subType.
+
+CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
+
+Lemma SubP u : Sub_spec u.
+Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
+
+Lemma SubK x Px : @val sT (Sub x Px) = x.
+Proof. by case: sT. Qed.
+
+Definition insub x :=
+ if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None.
+
+Definition insubd u0 x := odflt u0 (insub x).
+
+CoInductive insub_spec x : option sT -> Type :=
+ | InsubSome u of P x & val u = x : insub_spec x (Some u)
+ | InsubNone of ~~ P x : insub_spec x None.
+
+Lemma insubP x : insub_spec x (insub x).
+Proof.
+by rewrite /insub; case: {-}_ / idP; [left; rewrite ?SubK | right; apply/negP].
+Qed.
+
+Lemma insubT x Px : insub x = Some (Sub x Px).
+Admitted.
+
+Lemma insubF x : P x = false -> insub x = None.
+Proof. by move/idP; case: insubP. Qed.
+
+Lemma insubN x : ~~ P x -> insub x = None.
+Proof. by move/negPf/insubF. Qed.
+
+Lemma isSome_insub : ([eta insub] : pred T) =1 P.
+Proof. by apply: fsym => x; case: insubP => // /negPf. Qed.
+
+Lemma insubK : ocancel insub (@val _).
+Proof. by move=> x; case: insubP. Qed.
+
+Lemma valP (u : sT) : P (val u).
+Proof. by case/SubP: u => x Px; rewrite SubK. Qed.
+
+Lemma valK : pcancel (@val _) insub.
+Proof. by case/SubP=> x Px; rewrite SubK; apply: insubT. Qed.
+
+Lemma val_inj : injective (@val sT).
+Proof. exact: pcan_inj valK. Qed.
+
+Lemma valKd u0 : cancel (@val _) (insubd u0).
+Proof. by move=> u; rewrite /insubd valK. Qed.
+
+Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0.
+Proof. by rewrite /insubd; case: insubP => [u -> | /negPf->]. Qed.
+
+Lemma insubdK u0 : {in P, cancel (insubd u0) (@val _)}.
+Proof. by move=> x Px; rewrite /= val_insubd [P x]Px. Qed.
+
+Definition insub_eq x :=
+ let Some_sub Px := Some (Sub x Px : sT) in
+ let None_sub _ := None in
+ (if P x as Px return P x = Px -> _ then Some_sub else None_sub) (erefl _).
+
+Lemma insub_eqE : insub_eq =1 insub.
+Proof.
+rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'.
+by congr (Some _); apply: val_inj; rewrite !SubK.
+Qed.
+
+End SubType.
+
+Arguments SubType [T P].
+Arguments Sub [T P s].
+Arguments vrefl [T P].
+Arguments vrefl_rect [T P].
+Arguments clone_subType [T P] U v [sT] _ [c Urec cK].
+Arguments insub [T P sT].
+Arguments insubT [T] P [sT x].
+Arguments val_inj [T P sT].
+Prenex Implicits val Sub vrefl vrefl_rect insub insubd val_inj.
+
+Local Notation inlined_sub_rect :=
+ (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px).
+
+Local Notation inlined_new_rect :=
+ (fun K K_S u => let (x) as u return K u := u in K_S x).
+
+Notation "[ 'subType' 'for' v ]" := (SubType _ v _ inlined_sub_rect vrefl_rect)
+ (at level 0, only parsing) : form_scope.
+
+Notation "[ 'sub' 'Type' 'for' v ]" := (SubType _ v _ _ vrefl_rect)
+ (at level 0, format "[ 'sub' 'Type' 'for' v ]") : form_scope.
+
+Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl)
+ (at level 0, format "[ 'subType' 'for' v 'by' rec ]") : form_scope.
+
+Notation "[ 'subType' 'of' U 'for' v ]" := (clone_subType U v id idfun)
+ (at level 0, format "[ 'subType' 'of' U 'for' v ]") : form_scope.
+
+(*
+Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun)
+ (at level 0, format "[ 'subType' 'for' v ]") : form_scope.
+*)
+Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id)
+ (at level 0, format "[ 'subType' 'of' U ]") : form_scope.
+
+Definition NewType T U v c Urec :=
+ let Urec' P IH := Urec P (fun x : T => IH x isT : P _) in
+ SubType U v (fun x _ => c x) Urec'.
+Arguments NewType [T U].
+
+Notation "[ 'newType' 'for' v ]" := (NewType v _ inlined_new_rect vrefl_rect)
+ (at level 0, only parsing) : form_scope.
+
+Notation "[ 'new' 'Type' 'for' v ]" := (NewType v _ _ vrefl_rect)
+ (at level 0, format "[ 'new' 'Type' 'for' v ]") : form_scope.
+
+Notation "[ 'newType' 'for' v 'by' rec ]" := (NewType v _ rec vrefl)
+ (at level 0, format "[ 'newType' 'for' v 'by' rec ]") : form_scope.
+
+Definition innew T nT x := @Sub T predT nT x (erefl true).
+Arguments innew [T nT].
+Prenex Implicits innew.
+
+Lemma innew_val T nT : cancel val (@innew T nT).
+Proof. by move=> u; apply: val_inj; apply: SubK. Qed.
+
+(* Prenex Implicits and renaming. *)
+Notation sval := (@proj1_sig _ _).
+Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'").
+
+Section SubEqType.
+
+Variables (T : eqType) (P : pred T) (sT : subType P).
+
+Local Notation ev_ax := (fun T v => @Equality.axiom T (fun x y => v x == v y)).
+Lemma val_eqP : ev_ax sT val. Proof. exact: inj_eqAxiom val_inj. Qed.
+
+Definition sub_eqMixin := EqMixin val_eqP.
+Canonical sub_eqType := Eval hnf in EqType sT sub_eqMixin.
+
+Definition SubEqMixin :=
+ (let: SubType _ v _ _ _ as sT' := sT
+ return ev_ax sT' val -> Equality.class_of sT' in
+ fun vP : ev_ax _ v => EqMixin vP
+ ) val_eqP.
+
+Lemma val_eqE (u v : sT) : (val u == val v) = (u == v).
+Proof. by []. Qed.
+
+End SubEqType.
+
+Arguments val_eqP [T P sT x y].
+Prenex Implicits val_eqP.
+
+Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
+ (at level 0, format "[ 'eqMixin' 'of' T 'by' <: ]") : form_scope.
+
+(* ssrnat ---------------------------------------------------------- *)
+
+Notation succn := Datatypes.S.
+Notation predn := Peano.pred.
+
+Notation "n .+1" := (succn n) (at level 2, left associativity,
+ format "n .+1") : nat_scope.
+Notation "n .+2" := n.+1.+1 (at level 2, left associativity,
+ format "n .+2") : nat_scope.
+Notation "n .+3" := n.+2.+1 (at level 2, left associativity,
+ format "n .+3") : nat_scope.
+Notation "n .+4" := n.+2.+2 (at level 2, left associativity,
+ format "n .+4") : nat_scope.
+
+Notation "n .-1" := (predn n) (at level 2, left associativity,
+ format "n .-1") : nat_scope.
+Notation "n .-2" := n.-1.-1 (at level 2, left associativity,
+ format "n .-2") : nat_scope.
+
+Fixpoint eqn m n {struct m} :=
+ match m, n with
+ | 0, 0 => true
+ | m'.+1, n'.+1 => eqn m' n'
+ | _, _ => false
+ end.
+
+Lemma eqnP : Equality.axiom eqn.
+Proof.
+move=> n m; apply: (iffP idP) => [|<-]; last by elim n.
+by elim: n m => [|n IHn] [|m] //= /IHn->.
+Qed.
+
+Canonical nat_eqMixin := EqMixin eqnP.
+Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
+
+Arguments eqnP [x y].
+Prenex Implicits eqnP.
+
+Coercion nat_of_bool (b : bool) := if b then 1 else 0.
+
+Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false.
+
+Lemma oddb (b : bool) : odd b = b. Proof. by case: b. Qed.
+
+Definition subn_rec := minus.
+Notation "m - n" := (subn_rec m n) : nat_rec_scope.
+
+Definition subn := nosimpl subn_rec.
+Notation "m - n" := (subn m n) : nat_scope.
+
+Definition leq m n := m - n == 0.
+
+Notation "m <= n" := (leq m n) : nat_scope.
+Notation "m < n" := (m.+1 <= n) : nat_scope.
+Notation "m >= n" := (n <= m) (only parsing) : nat_scope.
+Notation "m > n" := (n < m) (only parsing) : nat_scope.
+
+
+Notation "m <= n <= p" := ((m <= n) && (n <= p)) : nat_scope.
+Notation "m < n <= p" := ((m < n) && (n <= p)) : nat_scope.
+Notation "m <= n < p" := ((m <= n) && (n < p)) : nat_scope.
+Notation "m < n < p" := ((m < n) && (n < p)) : nat_scope.
+
+Open Scope nat_scope.
+
+
+Lemma ltnS m n : (m < n.+1) = (m <= n). Proof. by []. Qed.
+Lemma leq0n n : 0 <= n. Proof. by []. Qed.
+Lemma ltn0Sn n : 0 < n.+1. Proof. by []. Qed.
+Lemma ltn0 n : n < 0 = false. Proof. by []. Qed.
+Lemma leqnn n : n <= n. Proof. by elim: n. Qed.
+Hint Resolve leqnn.
+Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed.
+
+Lemma leq_trans n m p : m <= n -> n <= p -> m <= p.
+Admitted.
+Lemma leqW m n : m <= n -> m <= n.+1.
+Admitted.
+Hint Resolve leqnSn.
+Lemma ltnW m n : m < n -> m <= n.
+Proof. exact: leq_trans. Qed.
+Hint Resolve ltnW.
+
+Definition addn_rec := plus.
+Notation "m + n" := (addn_rec m n) : nat_rec_scope.
+
+Definition addn := nosimpl addn_rec.
+Notation "m + n" := (addn m n) : nat_scope.
+
+Lemma addn0 : right_id 0 addn. Proof. by move=> n; apply/eqP; elim: n. Qed.
+Lemma add0n : left_id 0 addn. Proof. by []. Qed.
+Lemma addSn m n : m.+1 + n = (m + n).+1. Proof. by []. Qed.
+Lemma addnS m n : m + n.+1 = (m + n).+1. Proof. by elim: m. Qed.
+
+Lemma addnCA : left_commutative addn.
+Proof. by move=> m n p; elim: m => //= m; rewrite addnS => <-. Qed.
+
+Lemma addnC : commutative addn.
+Proof. by move=> m n; rewrite -{1}[n]addn0 addnCA addn0. Qed.
+
+Lemma addnA : associative addn.
+Proof. by move=> m n p; rewrite (addnC n) addnCA addnC. Qed.
+
+Lemma subnK m n : m <= n -> (n - m) + m = n.
+Admitted.
+
+
+Definition muln_rec := mult.
+Notation "m * n" := (muln_rec m n) : nat_rec_scope.
+
+Definition muln := nosimpl muln_rec.
+Notation "m * n" := (muln m n) : nat_scope.
+
+Lemma mul0n : left_zero 0 muln. Proof. by []. Qed.
+Lemma muln0 : right_zero 0 muln. Proof. by elim. Qed.
+Lemma mul1n : left_id 1 muln. Proof. exact: addn0. Qed.
+
+Lemma mulSn m n : m.+1 * n = n + m * n. Proof. by []. Qed.
+Lemma mulSnr m n : m.+1 * n = m * n + n. Proof. exact: addnC. Qed.
+
+Lemma mulnS m n : m * n.+1 = m + m * n.
+Proof. by elim: m => // m; rewrite !mulSn !addSn addnCA => ->. Qed.
+
+Lemma mulnSr m n : m * n.+1 = m * n + m.
+Proof. by rewrite addnC mulnS. Qed.
+
+Lemma muln1 : right_id 1 muln.
+Proof. by move=> n; rewrite mulnSr muln0. Qed.
+
+Lemma mulnC : commutative muln.
+Proof.
+by move=> m n; elim: m => [|m]; rewrite (muln0, mulnS) // mulSn => ->.
+Qed.
+
+Lemma mulnDl : left_distributive muln addn.
+Proof. by move=> m1 m2 n; elim: m1 => //= m1 IHm; rewrite -addnA -IHm. Qed.
+
+Lemma mulnDr : right_distributive muln addn.
+Proof. by move=> m n1 n2; rewrite !(mulnC m) mulnDl. Qed.
+
+Lemma mulnA : associative muln.
+Proof. by move=> m n p; elim: m => //= m; rewrite mulSn mulnDl => ->. Qed.
+
+Lemma mulnCA : left_commutative muln.
+Proof. by move=> m n1 n2; rewrite !mulnA (mulnC m). Qed.
+
+Lemma mulnAC : right_commutative muln.
+Proof. by move=> m n p; rewrite -!mulnA (mulnC n). Qed.
+
+Lemma mulnACA : interchange muln muln.
+Proof. by move=> m n p q; rewrite -!mulnA (mulnCA n). Qed.
+
+(* seq ------------------------------------------------------------- *)
+
+Delimit Scope seq_scope with SEQ.
+Open Scope seq_scope.
+
+(* Inductive seq (T : Type) : Type := Nil | Cons of T & seq T. *)
+Notation seq := list.
+Prenex Implicits cons.
+Notation Cons T := (@cons T) (only parsing).
+Notation Nil T := (@nil T) (only parsing).
+
+Bind Scope seq_scope with list.
+Arguments cons _%type _ _%SEQ.
+
+(* As :: and ++ are (improperly) declared in Init.datatypes, we only rebind *)
+(* them here. *)
+Infix "::" := cons : seq_scope.
+
+(* GG - this triggers a camlp4 warning, as if this Notation had been Reserved *)
+Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope.
+
+Notation "[ :: x1 ]" := (x1 :: [::])
+ (at level 0, format "[ :: x1 ]") : seq_scope.
+
+Notation "[ :: x & s ]" := (x :: s) (at level 0, only parsing) : seq_scope.
+
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+ (at level 0, format
+ "'[hv' [ :: '[' x1 , '/' x2 , '/' .. , '/' xn ']' '/ ' & s ] ']'"
+ ) : seq_scope.
+
+Notation "[ :: x1 ; x2 ; .. ; xn ]" := (x1 :: x2 :: .. [:: xn] ..)
+ (at level 0, format "[ :: '[' x1 ; '/' x2 ; '/' .. ; '/' xn ']' ]"
+ ) : seq_scope.
+
+Section Sequences.
+
+Variable n0 : nat. (* numerical parameter for take, drop et al *)
+Variable T : Type. (* must come before the implicit Type *)
+Variable x0 : T. (* default for head/nth *)
+
+Implicit Types x y z : T.
+Implicit Types m n : nat.
+Implicit Type s : seq T.
+
+Fixpoint size s := if s is _ :: s' then (size s').+1 else 0.
+
+Fixpoint cat s1 s2 := if s1 is x :: s1' then x :: s1' ++ s2 else s2
+where "s1 ++ s2" := (cat s1 s2) : seq_scope.
+
+Lemma cat0s s : [::] ++ s = s. Proof. by []. Qed.
+
+Lemma cats0 s : s ++ [::] = s.
+Proof. by elim: s => //= x s ->. Qed.
+
+Lemma catA s1 s2 s3 : s1 ++ s2 ++ s3 = (s1 ++ s2) ++ s3.
+Proof. by elim: s1 => //= x s1 ->. Qed.
+
+Fixpoint nth s n {struct n} :=
+ if s is x :: s' then if n is n'.+1 then @nth s' n' else x else x0.
+
+Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z].
+
+CoInductive last_spec : seq T -> Type :=
+ | LastNil : last_spec [::]
+ | LastRcons s x : last_spec (rcons s x).
+
+Lemma lastP s : last_spec s.
+Proof using. Admitted.
+
+Lemma last_ind P :
+ P [::] -> (forall s x, P s -> P (rcons s x)) -> forall s, P s.
+Proof using. Admitted.
+
+
+Section Map.
+
+Variables (T2 : Type) (f : T -> T2).
+
+Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
+
+End Map.
+
+Section SeqFind.
+
+Variable a : pred T.
+
+Fixpoint count s := if s is x :: s' then a x + count s' else 0.
+
+Fixpoint filter s :=
+ if s is x :: s' then if a x then x :: filter s' else filter s' else [::].
+
+End SeqFind.
+
+End Sequences.
+
+Infix "++" := cat : seq_scope.
+
+Notation count_mem x := (count (pred_of_simpl (pred1 x))).
+
+Section EqSeq.
+
+Variables (n0 : nat) (T : eqType) (x0 : T).
+Local Notation nth := (nth x0).
+Implicit Type s : seq T.
+Implicit Types x y z : T.
+
+Fixpoint eqseq s1 s2 {struct s2} :=
+ match s1, s2 with
+ | [::], [::] => true
+ | x1 :: s1', x2 :: s2' => (x1 == x2) && eqseq s1' s2'
+ | _, _ => false
+ end.
+
+Lemma eqseqP : Equality.axiom eqseq.
+Proof.
+move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl].
+case: (x1 =P x2) => [<-|neqx]; last by right; case.
+by apply: (iffP (IHs s2)) => [<-|[]].
+Qed.
+
+Canonical seq_eqMixin := EqMixin eqseqP.
+Canonical seq_eqType := Eval hnf in EqType (seq T) seq_eqMixin.
+
+Fixpoint mem_seq (s : seq T) :=
+ if s is y :: s' then xpredU1 y (mem_seq s') else xpred0.
+
+Definition eqseq_class := seq T.
+Identity Coercion seq_of_eqseq : eqseq_class >-> seq.
+Coercion pred_of_eq_seq (s : eqseq_class) : pred_class := [eta mem_seq s].
+
+Canonical seq_predType := @mkPredType T (seq T) pred_of_eq_seq.
+
+Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
+
+End EqSeq.
+
+Definition bitseq := seq bool.
+Canonical bitseq_eqType := Eval hnf in [eqType of bitseq].
+Canonical bitseq_predType := Eval hnf in [predType of bitseq].
+
+Section Pmap.
+
+Variables (aT rT : Type) (f : aT -> option rT) (g : rT -> aT).
+
+Fixpoint pmap s :=
+ if s is x :: s' then let r := pmap s' in oapp (cons^~ r) r (f x) else [::].
+
+End Pmap.
+
+Fixpoint iota m n := if n is n'.+1 then m :: iota m.+1 n' else [::].
+
+Section FoldRight.
+
+Variables (T : Type) (R : Type) (f : T -> R -> R) (z0 : R).
+
+Fixpoint foldr s := if s is x :: s' then f x (foldr s') else z0.
+
+End FoldRight.
+
+Lemma mem_iota m n i : (i \in iota m n) = (m <= i) && (i < m + n).
+Admitted.
+
+
+(* choice ------------------------------------------------------------- *)
+
+Module Choice.
+
+Section ClassDef.
+
+Record mixin_of T := Mixin {
+ find : pred T -> nat -> option T;
+ _ : forall P n x, find P n = Some x -> P x;
+ _ : forall P : pred T, (exists x, P x) -> exists n, find P n;
+ _ : forall P Q : pred T, P =1 Q -> find P =1 find Q
+}.
+
+Record class_of T := Class {base : Equality.class_of T; mixin : mixin_of T}.
+Local Coercion base : class_of >-> Equality.class_of.
+
+Structure type := Pack {sort; _ : class_of sort; _ : Type}.
+Local Coercion sort : type >-> Sortclass.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition pack m :=
+ fun b bT & phant_id (Equality.class bT) b => Pack (@Class T b m) T.
+
+(* Inheritance *)
+Definition eqType := @Equality.Pack cT xclass xT.
+
+End ClassDef.
+
+Module Import Exports.
+Coercion base : class_of >-> Equality.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Notation choiceType := type.
+Notation choiceMixin := mixin_of.
+Notation ChoiceType T m := (@pack T m _ _ id).
+Notation "[ 'choiceType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+ (at level 0, format "[ 'choiceType' 'of' T 'for' cT ]") : form_scope.
+Notation "[ 'choiceType' 'of' T ]" := (@clone T _ _ id)
+ (at level 0, format "[ 'choiceType' 'of' T ]") : form_scope.
+
+End Exports.
+
+End Choice.
+Export Choice.Exports.
+
+Section ChoiceTheory.
+
+Variable T : choiceType.
+
+Section CanChoice.
+
+Variables (sT : Type) (f : sT -> T).
+
+Lemma PcanChoiceMixin f' : pcancel f f' -> choiceMixin sT.
+Admitted.
+
+Definition CanChoiceMixin f' (fK : cancel f f') :=
+ PcanChoiceMixin (can_pcan fK).
+
+End CanChoice.
+
+Section SubChoice.
+
+Variables (P : pred T) (sT : subType P).
+
+Definition sub_choiceMixin := PcanChoiceMixin (@valK T P sT).
+Definition sub_choiceClass := @Choice.Class sT (sub_eqMixin sT) sub_choiceMixin.
+Canonical sub_choiceType := Choice.Pack sub_choiceClass sT.
+
+End SubChoice.
+
+
+Fact seq_choiceMixin : choiceMixin (seq T).
+Admitted.
+Canonical seq_choiceType := Eval hnf in ChoiceType (seq T) seq_choiceMixin.
+End ChoiceTheory.
+
+Fact nat_choiceMixin : choiceMixin nat.
+Proof.
+pose f := [fun (P : pred nat) n => if P n then Some n else None].
+exists f => [P n m | P [n Pn] | P Q eqPQ n] /=; last by rewrite eqPQ.
+ by case: ifP => // Pn [<-].
+by exists n; rewrite Pn.
+Qed.
+Canonical nat_choiceType := Eval hnf in ChoiceType nat nat_choiceMixin.
+
+Definition bool_choiceMixin := CanChoiceMixin oddb.
+Canonical bool_choiceType := Eval hnf in ChoiceType bool bool_choiceMixin.
+Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].
+
+
+Notation "[ 'choiceMixin' 'of' T 'by' <: ]" :=
+ (sub_choiceMixin _ : choiceMixin T)
+ (at level 0, format "[ 'choiceMixin' 'of' T 'by' <: ]") : form_scope.
+
+
+
+
+Module Countable.
+
+Record mixin_of (T : Type) : Type := Mixin {
+ pickle : T -> nat;
+ unpickle : nat -> option T;
+ pickleK : pcancel pickle unpickle
+}.
+
+Definition EqMixin T m := PcanEqMixin (@pickleK T m).
+Definition ChoiceMixin T m := PcanChoiceMixin (@pickleK T m).
+
+Section ClassDef.
+
+Record class_of T := Class { base : Choice.class_of T; mixin : mixin_of T }.
+Local Coercion base : class_of >-> Choice.class_of.
+
+Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
+Local Coercion sort : type >-> Sortclass.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition pack m :=
+ fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+
+End ClassDef.
+
+Module Exports.
+Coercion base : class_of >-> Choice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Coercion choiceType : type >-> Choice.type.
+Canonical choiceType.
+Notation countType := type.
+Notation CountType T m := (@pack T m _ _ id).
+Notation CountMixin := Mixin.
+Notation CountChoiceMixin := ChoiceMixin.
+Notation "[ 'countType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+ (at level 0, format "[ 'countType' 'of' T 'for' cT ]") : form_scope.
+Notation "[ 'countType' 'of' T ]" := (@clone T _ _ id)
+ (at level 0, format "[ 'countType' 'of' T ]") : form_scope.
+
+End Exports.
+
+End Countable.
+Export Countable.Exports.
+
+Definition unpickle T := Countable.unpickle (Countable.class T).
+Definition pickle T := Countable.pickle (Countable.class T).
+Arguments unpickle [T].
+Prenex Implicits pickle unpickle.
+
+Section CountableTheory.
+
+Variable T : countType.
+
+Lemma pickleK : @pcancel nat T pickle unpickle.
+Proof. exact: Countable.pickleK. Qed.
+
+Definition pickle_inv n :=
+ obind (fun x : T => if pickle x == n then Some x else None) (unpickle n).
+
+Lemma pickle_invK : ocancel pickle_inv pickle.
+Proof.
+by rewrite /pickle_inv => n; case def_x: (unpickle n) => //= [x]; case: eqP.
+Qed.
+
+Lemma pickleK_inv : pcancel pickle pickle_inv.
+Proof. by rewrite /pickle_inv => x; rewrite pickleK /= eqxx. Qed.
+
+Lemma pcan_pickleK sT f f' :
+ @pcancel T sT f f' -> pcancel (pickle \o f) (pcomp f' unpickle).
+Proof. by move=> fK x; rewrite /pcomp pickleK /= fK. Qed.
+
+Definition PcanCountMixin sT f f' (fK : pcancel f f') :=
+ @CountMixin sT _ _ (pcan_pickleK fK).
+
+Definition CanCountMixin sT f f' (fK : cancel f f') :=
+ @PcanCountMixin sT _ _ (can_pcan fK).
+
+Definition sub_countMixin P sT := PcanCountMixin (@valK T P sT).
+
+End CountableTheory.
+Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
+ (sub_countMixin _ : Countable.mixin_of T)
+ (at level 0, format "[ 'countMixin' 'of' T 'by' <: ]") : form_scope.
+
+Section SubCountType.
+
+Variables (T : choiceType) (P : pred T).
+Import Countable.
+
+Structure subCountType : Type :=
+ SubCountType {subCount_sort :> subType P; _ : mixin_of subCount_sort}.
+
+Coercion sub_countType (sT : subCountType) :=
+ Eval hnf in pack (let: SubCountType _ m := sT return mixin_of sT in m) id.
+Canonical sub_countType.
+
+Definition pack_subCountType U :=
+ fun sT cT & sub_sort sT * sort cT -> U * U =>
+ fun b m & phant_id (Class b m) (class cT) => @SubCountType sT m.
+
+End SubCountType.
+
+(* This assumes that T has both countType and subType structures. *)
+Notation "[ 'subCountType' 'of' T ]" :=
+ (@pack_subCountType _ _ T _ _ id _ _ id)
+ (at level 0, format "[ 'subCountType' 'of' T ]") : form_scope.
+
+Lemma nat_pickleK : pcancel id (@Some nat). Proof. by []. Qed.
+Definition nat_countMixin := CountMixin nat_pickleK.
+Canonical nat_countType := Eval hnf in CountType nat nat_countMixin.
+
+(* fintype --------------------------------------------------------- *)
+
+Module Finite.
+
+Section RawMixin.
+
+Variable T : eqType.
+
+Definition axiom e := forall x : T, count_mem x e = 1.
+
+Lemma uniq_enumP e : uniq e -> e =i T -> axiom e.
+Admitted.
+
+Record mixin_of := Mixin {
+ mixin_base : Countable.mixin_of T;
+ mixin_enum : seq T;
+ _ : axiom mixin_enum
+}.
+
+End RawMixin.
+
+Section Mixins.
+
+Variable T : countType.
+
+Definition EnumMixin :=
+ let: Countable.Pack _ (Countable.Class _ m) _ as cT := T
+ return forall e : seq cT, axiom e -> mixin_of cT in
+ @Mixin (EqType _ _) m.
+
+Definition UniqMixin e Ue eT := @EnumMixin e (uniq_enumP Ue eT).
+
+Variable n : nat.
+
+End Mixins.
+
+Section ClassDef.
+
+Record class_of T := Class {
+ base : Choice.class_of T;
+ mixin : mixin_of (Equality.Pack base T)
+}.
+Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)).
+Local Coercion base : class_of >-> Choice.class_of.
+
+Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
+Local Coercion sort : type >-> Sortclass.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+
+Definition pack b0 (m0 : mixin_of (EqType T b0)) :=
+ fun bT b & phant_id (Choice.class bT) b =>
+ fun m & phant_id m0 m => Pack (@Class T b m) T.
+
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (base2 xclass) xT.
+
+End ClassDef.
+
+Module Import Exports.
+Coercion mixin_base : mixin_of >-> Countable.mixin_of.
+Coercion base : class_of >-> Choice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion base2 : class_of >-> Countable.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Coercion choiceType : type >-> Choice.type.
+Canonical choiceType.
+Coercion countType : type >-> Countable.type.
+Canonical countType.
+Notation finType := type.
+Notation FinType T m := (@pack T _ m _ _ id _ id).
+Notation FinMixin := EnumMixin.
+Notation UniqFinMixin := UniqMixin.
+Notation "[ 'finType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+ (at level 0, format "[ 'finType' 'of' T 'for' cT ]") : form_scope.
+Notation "[ 'finType' 'of' T ]" := (@clone T _ _ id)
+ (at level 0, format "[ 'finType' 'of' T ]") : form_scope.
+End Exports.
+
+Module Type EnumSig.
+Parameter enum : forall cT : type, seq cT.
+Axiom enumDef : enum = fun cT => mixin_enum (class cT).
+End EnumSig.
+
+Module EnumDef : EnumSig.
+Definition enum cT := mixin_enum (class cT).
+Definition enumDef := erefl enum.
+End EnumDef.
+
+Notation enum := EnumDef.enum.
+
+End Finite.
+Export Finite.Exports.
+
+Section SubFinType.
+
+Variables (T : choiceType) (P : pred T).
+Import Finite.
+
+Structure subFinType := SubFinType {
+ subFin_sort :> subType P;
+ _ : mixin_of (sub_eqType subFin_sort)
+}.
+
+Definition pack_subFinType U :=
+ fun cT b m & phant_id (class cT) (@Class U b m) =>
+ fun sT m' & phant_id m' m => @SubFinType sT m'.
+
+Implicit Type sT : subFinType.
+
+Definition subFin_mixin sT :=
+ let: SubFinType _ m := sT return mixin_of (sub_eqType sT) in m.
+
+Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT).
+Canonical subFinType_subCountType.
+
+Coercion subFinType_finType sT :=
+ Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)) sT.
+Canonical subFinType_finType.
+
+Definition enum_mem T (mA : mem_pred _) := filter mA (Finite.enum T).
+Definition image_mem T T' f mA : seq T' := map f (@enum_mem T mA).
+Definition codom T T' f := @image_mem T T' f (mem T).
+
+Lemma codom_val sT x : (x \in codom (val : sT -> T)) = P x.
+Admitted.
+
+End SubFinType.
+
+
+(* This assumes that T has both finType and subCountType structures. *)
+Notation "[ 'subFinType' 'of' T ]" := (@pack_subFinType _ _ T _ _ _ id _ _ id)
+ (at level 0, format "[ 'subFinType' 'of' T ]") : form_scope.
+
+
+
+Section OrdinalSub.
+
+Variable n : nat.
+
+Inductive ordinal : predArgType := Ordinal m of m < n.
+
+Coercion nat_of_ord i := let: Ordinal m _ := i in m.
+
+Canonical ordinal_subType := [subType for nat_of_ord].
+Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:].
+Canonical ordinal_eqType := Eval hnf in EqType ordinal ordinal_eqMixin.
+Definition ordinal_choiceMixin := [choiceMixin of ordinal by <:].
+Canonical ordinal_choiceType :=
+ Eval hnf in ChoiceType ordinal ordinal_choiceMixin.
+Definition ordinal_countMixin := [countMixin of ordinal by <:].
+Canonical ordinal_countType := Eval hnf in CountType ordinal ordinal_countMixin.
+Canonical ordinal_subCountType := [subCountType of ordinal].
+
+Lemma ltn_ord (i : ordinal) : i < n. Proof. exact: valP i. Qed.
+
+Lemma ord_inj : injective nat_of_ord. Proof. exact: val_inj. Qed.
+
+Definition ord_enum : seq ordinal := pmap insub (iota 0 n).
+
+Lemma val_ord_enum : map val ord_enum = iota 0 n.
+Admitted.
+
+Lemma ord_enum_uniq : uniq ord_enum.
+Admitted.
+
+Lemma mem_ord_enum i : i \in ord_enum.
+Admitted.
+
+Definition ordinal_finMixin :=
+ Eval hnf in UniqFinMixin ord_enum_uniq mem_ord_enum.
+Canonical ordinal_finType := Eval hnf in FinType ordinal ordinal_finMixin.
+Canonical ordinal_subFinType := Eval hnf in [subFinType of ordinal].
+
+End OrdinalSub.
+
+Notation "''I_' n" := (ordinal n)
+ (at level 8, n at level 2, format "''I_' n").
+
+(* bigop ----------------------------------------------------------------- *)
+
+Reserved Notation "\big [ op / idx ]_ i F"
+ (at level 36, F at level 36, op, idx at level 10, i at level 0,
+ right associativity,
+ format "'[' \big [ op / idx ]_ i '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i <- r | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, r at level 50,
+ format "'[' \big [ op / idx ]_ ( i <- r | P ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i <- r ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, r at level 50,
+ format "'[' \big [ op / idx ]_ ( i <- r ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50,
+ format "'[' \big [ op / idx ]_ ( m <= i < n | P ) F ']'").
+Reserved Notation "\big [ op / idx ]_ ( m <= i < n ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, m, n at level 50,
+ format "'[' \big [ op / idx ]_ ( m <= i < n ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, i at level 50,
+ format "'[' \big [ op / idx ]_ ( i | P ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i : t | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, i at level 50,
+ format "'[' \big [ op / idx ]_ ( i : t | P ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i : t ) F"
+ (at level 36, F at level 36, op, idx at level 10, i at level 50,
+ format "'[' \big [ op / idx ]_ ( i : t ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i < n | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, n at level 50,
+ format "'[' \big [ op / idx ]_ ( i < n | P ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i < n ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, n at level 50,
+ format "'[' \big [ op / idx ]_ ( i < n ) F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i 'in' A | P ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, A at level 50,
+ format "'[' \big [ op / idx ]_ ( i 'in' A | P ) '/ ' F ']'").
+Reserved Notation "\big [ op / idx ]_ ( i 'in' A ) F"
+ (at level 36, F at level 36, op, idx at level 10, i, A at level 50,
+ format "'[' \big [ op / idx ]_ ( i 'in' A ) '/ ' F ']'").
+
+Module Monoid.
+
+Section Definitions.
+Variables (T : Type) (idm : T).
+
+Structure law := Law {
+ operator : T -> T -> T;
+ _ : associative operator;
+ _ : left_id idm operator;
+ _ : right_id idm operator
+}.
+Local Coercion operator : law >-> Funclass.
+
+Structure com_law := ComLaw {
+ com_operator : law;
+ _ : commutative com_operator
+}.
+Local Coercion com_operator : com_law >-> law.
+
+Structure mul_law := MulLaw {
+ mul_operator : T -> T -> T;
+ _ : left_zero idm mul_operator;
+ _ : right_zero idm mul_operator
+}.
+Local Coercion mul_operator : mul_law >-> Funclass.
+
+Structure add_law (mul : T -> T -> T) := AddLaw {
+ add_operator : com_law;
+ _ : left_distributive mul add_operator;
+ _ : right_distributive mul add_operator
+}.
+Local Coercion add_operator : add_law >-> com_law.
+
+Let op_id (op1 op2 : T -> T -> T) := phant_id op1 op2.
+
+Definition clone_law op :=
+ fun (opL : law) & op_id opL op =>
+ fun opmA op1m opm1 (opL' := @Law op opmA op1m opm1)
+ & phant_id opL' opL => opL'.
+
+Definition clone_com_law op :=
+ fun (opL : law) (opC : com_law) & op_id opL op & op_id opC op =>
+ fun opmC (opC' := @ComLaw opL opmC) & phant_id opC' opC => opC'.
+
+Definition clone_mul_law op :=
+ fun (opM : mul_law) & op_id opM op =>
+ fun op0m opm0 (opM' := @MulLaw op op0m opm0) & phant_id opM' opM => opM'.
+
+Definition clone_add_law mop aop :=
+ fun (opC : com_law) (opA : add_law mop) & op_id opC aop & op_id opA aop =>
+ fun mopDm mopmD (opA' := @AddLaw mop opC mopDm mopmD)
+ & phant_id opA' opA => opA'.
+
+End Definitions.
+
+Module Import Exports.
+Coercion operator : law >-> Funclass.
+Coercion com_operator : com_law >-> law.
+Coercion mul_operator : mul_law >-> Funclass.
+Coercion add_operator : add_law >-> com_law.
+Notation "[ 'law' 'of' f ]" := (@clone_law _ _ f _ id _ _ _ id)
+ (at level 0, format"[ 'law' 'of' f ]") : form_scope.
+Notation "[ 'com_law' 'of' f ]" := (@clone_com_law _ _ f _ _ id id _ id)
+ (at level 0, format "[ 'com_law' 'of' f ]") : form_scope.
+Notation "[ 'mul_law' 'of' f ]" := (@clone_mul_law _ _ f _ id _ _ id)
+ (at level 0, format"[ 'mul_law' 'of' f ]") : form_scope.
+Notation "[ 'add_law' m 'of' a ]" := (@clone_add_law _ _ m a _ _ id id _ _ id)
+ (at level 0, format "[ 'add_law' m 'of' a ]") : form_scope.
+End Exports.
+
+Section CommutativeAxioms.
+
+Variable (T : Type) (zero one : T) (mul add : T -> T -> T) (inv : T -> T).
+Hypothesis mulC : commutative mul.
+
+Lemma mulC_id : left_id one mul -> right_id one mul.
+Proof. by move=> mul1x x; rewrite mulC. Qed.
+
+Lemma mulC_zero : left_zero zero mul -> right_zero zero mul.
+Proof. by move=> mul0x x; rewrite mulC. Qed.
+
+Lemma mulC_dist : left_distributive mul add -> right_distributive mul add.
+Proof. by move=> mul_addl x y z; rewrite !(mulC x). Qed.
+
+End CommutativeAxioms.
+Module Theory.
+
+Section Theory.
+Variables (T : Type) (idm : T).
+
+Section Plain.
+Variable mul : law idm.
+Lemma mul1m : left_id idm mul. Proof. by case mul. Qed.
+Lemma mulm1 : right_id idm mul. Proof. by case mul. Qed.
+Lemma mulmA : associative mul. Proof. by case mul. Qed.
+(*Lemma iteropE n x : iterop n mul x idm = iter n (mul x) idm.*)
+
+End Plain.
+
+Section Commutative.
+Variable mul : com_law idm.
+Lemma mulmC : commutative mul. Proof. by case mul. Qed.
+Lemma mulmCA : left_commutative mul.
+Proof. by move=> x y z; rewrite !mulmA (mulmC x). Qed.
+Lemma mulmAC : right_commutative mul.
+Proof. by move=> x y z; rewrite -!mulmA (mulmC y). Qed.
+Lemma mulmACA : interchange mul mul.
+Proof. by move=> x y z t; rewrite -!mulmA (mulmCA y). Qed.
+End Commutative.
+
+Section Mul.
+Variable mul : mul_law idm.
+Lemma mul0m : left_zero idm mul. Proof. by case mul. Qed.
+Lemma mulm0 : right_zero idm mul. Proof. by case mul. Qed.
+End Mul.
+
+Section Add.
+Variables (mul : T -> T -> T) (add : add_law idm mul).
+Lemma addmA : associative add. Proof. exact: mulmA. Qed.
+Lemma addmC : commutative add. Proof. exact: mulmC. Qed.
+Lemma addmCA : left_commutative add. Proof. exact: mulmCA. Qed.
+Lemma addmAC : right_commutative add. Proof. exact: mulmAC. Qed.
+Lemma add0m : left_id idm add. Proof. exact: mul1m. Qed.
+Lemma addm0 : right_id idm add. Proof. exact: mulm1. Qed.
+Lemma mulm_addl : left_distributive mul add. Proof. by case add. Qed.
+Lemma mulm_addr : right_distributive mul add. Proof. by case add. Qed.
+End Add.
+
+Definition simpm := (mulm1, mulm0, mul1m, mul0m, mulmA).
+
+End Theory.
+
+End Theory.
+Include Theory.
+
+End Monoid.
+Export Monoid.Exports.
+
+Section PervasiveMonoids.
+
+Import Monoid.
+
+Canonical andb_monoid := Law andbA andTb andbT.
+Canonical andb_comoid := ComLaw andbC.
+
+Canonical andb_muloid := MulLaw andFb andbF.
+Canonical orb_monoid := Law orbA orFb orbF.
+Canonical orb_comoid := ComLaw orbC.
+Canonical orb_muloid := MulLaw orTb orbT.
+Canonical addb_monoid := Law addbA addFb addbF.
+Canonical addb_comoid := ComLaw addbC.
+Canonical orb_addoid := AddLaw andb_orl andb_orr.
+Canonical andb_addoid := AddLaw orb_andl orb_andr.
+Canonical addb_addoid := AddLaw andb_addl andb_addr.
+
+Canonical addn_monoid := Law addnA add0n addn0.
+Canonical addn_comoid := ComLaw addnC.
+Canonical muln_monoid := Law mulnA mul1n muln1.
+Canonical muln_comoid := ComLaw mulnC.
+Canonical muln_muloid := MulLaw mul0n muln0.
+Canonical addn_addoid := AddLaw mulnDl mulnDr.
+
+Canonical cat_monoid T := Law (@catA T) (@cat0s T) (@cats0 T).
+
+End PervasiveMonoids.
+Delimit Scope big_scope with BIG.
+Open Scope big_scope.
+
+(* The bigbody wrapper is a workaround for a quirk of the Coq pretty-printer, *)
+(* which would fail to redisplay the \big notation when the <general_term> or *)
+(* <condition> do not depend on the bound index. The BigBody constructor *)
+(* packages both in in a term in which i occurs; it also depends on the *)
+(* iterated <op>, as this can give more information on the expected type of *)
+(* the <general_term>, thus allowing for the insertion of coercions. *)
+CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+
+Definition applybig {R I} (body : bigbody R I) x :=
+ let: BigBody _ op b v := body in if b then op v x else x.
+
+Definition reducebig R I idx r (body : I -> bigbody R I) :=
+ foldr (applybig \o body) idx r.
+
+Module Type BigOpSig.
+Parameter bigop : forall R I, R -> seq I -> (I -> bigbody R I) -> R.
+Axiom bigopE : bigop = reducebig.
+End BigOpSig.
+
+Module BigOp : BigOpSig.
+Definition bigop := reducebig.
+Lemma bigopE : bigop = reducebig. Proof. by []. Qed.
+End BigOp.
+
+Notation bigop := BigOp.bigop (only parsing).
+Canonical bigop_unlock := Unlockable BigOp.bigopE.
+
+Definition index_iota m n := iota m (n - m).
+
+Definition index_enum (T : finType) := Finite.enum T.
+
+Lemma mem_index_iota m n i : i \in index_iota m n = (m <= i < n).
+Admitted.
+
+Lemma mem_index_enum T i : i \in index_enum T.
+Admitted.
+
+Hint Resolve mem_index_enum.
+
+(*
+Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
+Proof. by []. Qed.
+*)
+
+Notation "\big [ op / idx ]_ ( i <- r | P ) F" :=
+ (bigop idx r (fun i => BigBody i op P%B F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i <- r ) F" :=
+ (bigop idx r (fun i => BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
+ (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%B F))
+ : big_scope.
+Notation "\big [ op / idx ]_ ( m <= i < n ) F" :=
+ (bigop idx (index_iota m n) (fun i : nat => BigBody i op true F))
+ : big_scope.
+Notation "\big [ op / idx ]_ ( i | P ) F" :=
+ (bigop idx (index_enum _) (fun i => BigBody i op P%B F)) : big_scope.
+Notation "\big [ op / idx ]_ i F" :=
+ (bigop idx (index_enum _) (fun i => BigBody i op true F)) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t | P ) F" :=
+ (bigop idx (index_enum _) (fun i : t => BigBody i op P%B F))
+ (only parsing) : big_scope.
+Notation "\big [ op / idx ]_ ( i : t ) F" :=
+ (bigop idx (index_enum _) (fun i : t => BigBody i op true F))
+ (only parsing) : big_scope.
+Notation "\big [ op / idx ]_ ( i < n | P ) F" :=
+ (\big[op/idx]_(i : ordinal n | P%B) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i < n ) F" :=
+ (\big[op/idx]_(i : ordinal n) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i 'in' A | P ) F" :=
+ (\big[op/idx]_(i | (i \in A) && P) F) : big_scope.
+Notation "\big [ op / idx ]_ ( i 'in' A ) F" :=
+ (\big[op/idx]_(i | i \in A) F) : big_scope.
+
+Notation BIG_F := (F in \big[_/_]_(i <- _ | _) F i)%pattern.
+Notation BIG_P := (P in \big[_/_]_(i <- _ | P i) _)%pattern.
+
+(* Induction loading *)
+Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
+ K (\big[op/idx]_(i <- r | P i) F i) * K' (\big[op/idx]_(i <- r | P i) F i)
+ -> K' (\big[op/idx]_(i <- r | P i) F i).
+Proof. by case. Qed.
+
+Arguments big_load [R] K [K'] idx op [I].
+
+Section Elim3.
+
+Variables (R1 R2 R3 : Type) (K : R1 -> R2 -> R3 -> Type).
+Variables (id1 : R1) (op1 : R1 -> R1 -> R1).
+Variables (id2 : R2) (op2 : R2 -> R2 -> R2).
+Variables (id3 : R3) (op3 : R3 -> R3 -> R3).
+
+Hypothesis Kid : K id1 id2 id3.
+
+Lemma big_rec3 I r (P : pred I) F1 F2 F3
+ (K_F : forall i y1 y2 y3, P i -> K y1 y2 y3 ->
+ K (op1 (F1 i) y1) (op2 (F2 i) y2) (op3 (F3 i) y3)) :
+ K (\big[op1/id1]_(i <- r | P i) F1 i)
+ (\big[op2/id2]_(i <- r | P i) F2 i)
+ (\big[op3/id3]_(i <- r | P i) F3 i).
+Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed.
+
+Hypothesis Kop : forall x1 x2 x3 y1 y2 y3,
+ K x1 x2 x3 -> K y1 y2 y3-> K (op1 x1 y1) (op2 x2 y2) (op3 x3 y3).
+Lemma big_ind3 I r (P : pred I) F1 F2 F3
+ (K_F : forall i, P i -> K (F1 i) (F2 i) (F3 i)) :
+ K (\big[op1/id1]_(i <- r | P i) F1 i)
+ (\big[op2/id2]_(i <- r | P i) F2 i)
+ (\big[op3/id3]_(i <- r | P i) F3 i).
+Proof. by apply: big_rec3 => i x1 x2 x3 /K_F; apply: Kop. Qed.
+
+End Elim3.
+
+Arguments big_rec3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ [I r P F1 F2 F3].
+Arguments big_ind3 [R1 R2 R3] K [id1 op1 id2 op2 id3 op3] _ _ [I r P F1 F2 F3].
+
+Section Elim2.
+
+Variables (R1 R2 : Type) (K : R1 -> R2 -> Type) (f : R2 -> R1).
+Variables (id1 : R1) (op1 : R1 -> R1 -> R1).
+Variables (id2 : R2) (op2 : R2 -> R2 -> R2).
+
+Hypothesis Kid : K id1 id2.
+
+Lemma big_rec2 I r (P : pred I) F1 F2
+ (K_F : forall i y1 y2, P i -> K y1 y2 ->
+ K (op1 (F1 i) y1) (op2 (F2 i) y2)) :
+ K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).
+Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: K_F. Qed.
+
+Hypothesis Kop : forall x1 x2 y1 y2,
+ K x1 x2 -> K y1 y2 -> K (op1 x1 y1) (op2 x2 y2).
+Lemma big_ind2 I r (P : pred I) F1 F2 (K_F : forall i, P i -> K (F1 i) (F2 i)) :
+ K (\big[op1/id1]_(i <- r | P i) F1 i) (\big[op2/id2]_(i <- r | P i) F2 i).
+Proof. by apply: big_rec2 => i x1 x2 /K_F; apply: Kop. Qed.
+
+Hypotheses (f_op : {morph f : x y / op2 x y >-> op1 x y}) (f_id : f id2 = id1).
+Lemma big_morph I r (P : pred I) F :
+ f (\big[op2/id2]_(i <- r | P i) F i) = \big[op1/id1]_(i <- r | P i) f (F i).
+Proof. by rewrite unlock; elim: r => //= i r <-; rewrite -f_op -fun_if. Qed.
+
+End Elim2.
+
+Arguments big_rec2 [R1 R2] K [id1 op1 id2 op2] _ [I r P F1 F2].
+Arguments big_ind2 [R1 R2] K [id1 op1 id2 op2] _ _ [I r P F1 F2].
+Arguments big_morph [R1 R2] f [id1 op1 id2 op2] _ _ [I].
+
+Section Elim1.
+
+Variables (R : Type) (K : R -> Type) (f : R -> R).
+Variables (idx : R) (op op' : R -> R -> R).
+
+Hypothesis Kid : K idx.
+
+Lemma big_rec I r (P : pred I) F
+ (Kop : forall i x, P i -> K x -> K (op (F i) x)) :
+ K (\big[op/idx]_(i <- r | P i) F i).
+Proof. by rewrite unlock; elim: r => //= i r; case: ifP => //; apply: Kop. Qed.
+
+Hypothesis Kop : forall x y, K x -> K y -> K (op x y).
+Lemma big_ind I r (P : pred I) F (K_F : forall i, P i -> K (F i)) :
+ K (\big[op/idx]_(i <- r | P i) F i).
+Proof. by apply: big_rec => // i x /K_F /Kop; apply. Qed.
+
+Hypothesis Kop' : forall x y, K x -> K y -> op x y = op' x y.
+Lemma eq_big_op I r (P : pred I) F (K_F : forall i, P i -> K (F i)) :
+ \big[op/idx]_(i <- r | P i) F i = \big[op'/idx]_(i <- r | P i) F i.
+Proof.
+by elim/(big_load K): _; elim/big_rec2: _ => // i _ y Pi [Ky <-]; auto.
+Qed.
+
+Hypotheses (fM : {morph f : x y / op x y}) (f_id : f idx = idx).
+Lemma big_endo I r (P : pred I) F :
+ f (\big[op/idx]_(i <- r | P i) F i) = \big[op/idx]_(i <- r | P i) f (F i).
+Proof. exact: big_morph. Qed.
+
+End Elim1.
+
+Arguments big_rec [R] K [idx op] _ [I r P F].
+Arguments big_ind [R] K [idx op] _ _ [I r P F].
+Arguments eq_big_op [R] K [idx op] op' _ _ _ [I].
+Arguments big_endo [R] f [idx op] _ _ [I].
+
+(* zmodp -------------------------------------------------------------------- *)
+
+Lemma ord1 : all_equal_to (@Ordinal 1 0 is_true_true : 'I_1).
+Admitted.
diff --git a/test-suite/prerequisite/ssr_ssrsyntax1.v b/test-suite/prerequisite/ssr_ssrsyntax1.v
new file mode 100644
index 000000000..2b404e2de
--- /dev/null
+++ b/test-suite/prerequisite/ssr_ssrsyntax1.v
@@ -0,0 +1,36 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require ssreflect.
+Require Import Arith.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Abort.
+
+Module Foo.
+Import ssreflect.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite 2![_ + _]plus_comm.
+split.
+Abort.
+End Foo.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Abort.
diff --git a/test-suite/ssr/absevarprop.v b/test-suite/ssr/absevarprop.v
new file mode 100644
index 000000000..fa1de0095
--- /dev/null
+++ b/test-suite/ssr/absevarprop.v
@@ -0,0 +1,96 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect ssrbool ssrfun.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y.
+move=> y x le_1 defx; rewrite insubT ?(leq_trans le_1) // => ?.
+by congr (Some _); apply: val_inj=> /=; exact: defx.
+Qed.
+
+Axiom P : nat -> Prop.
+Axiom Q : forall n, P n -> Prop.
+Definition R := fun (x : nat) (p : P x) m (q : P (x+1)) => m > 0.
+
+Inductive myEx : Type := ExI : forall n (pn : P n) pn', Q n pn -> R n pn n pn' -> myEx.
+
+Variable P1 : P 1.
+Variable P11 : P (1 + 1).
+Variable Q1 : forall P1, Q 1 P1.
+
+Lemma testmE1 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+ match goal with |- P 1 => exact: P1 | _ => fail end.
+ match goal with |- P (1+1) => exact: P11 | _ => fail end.
+ match goal with |- forall p : P 1, Q 1 p => move=> *; exact: Q1 | _ => fail end.
+match goal with |- forall (p : P 1) (q : P (1+1)), is_true (R 1 p 1 q) => done | _ => fail end.
+Qed.
+
+Lemma testE2 : exists y : { x | P x }, sval y = 1.
+Proof.
+apply: ex_intro (exist _ 1 _) _.
+ match goal with |- P 1 => exact: P1 | _ => fail end.
+match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
+Qed.
+
+Lemma testE3 : exists y : { x | P x }, sval y = 1.
+Proof.
+have := (ex_intro _ (exist _ 1 _) _); apply.
+ match goal with |- P 1 => exact: P1 | _ => fail end.
+match goal with |- forall p : P 1, @sval _ _ (@exist _ _ 1 p) = 1 => done | _ => fail end.
+Qed.
+
+Lemma testE4 : P 2 -> exists y : { x | P x }, sval y = 2.
+Proof.
+move=> P2; apply: ex_intro (exist _ 2 _) _.
+match goal with |- @sval _ _ (@exist _ _ 2 P2) = 2 => done | _ => fail end.
+Qed.
+
+Hint Resolve P1.
+
+Lemma testmE12 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+ match goal with |- P (1+1) => exact: P11 | _ => fail end.
+ match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
+match goal with |- forall (q : P (1+1)), is_true (R 1 P1 1 q) => done | _ => fail end.
+Qed.
+
+Create HintDb SSR.
+
+Hint Resolve P11 : SSR.
+
+Ltac ssrautoprop := trivial with SSR.
+
+Lemma testmE13 : myEx.
+Proof.
+apply: ExI 1 _ _ _ _.
+ match goal with |- Q 1 P1 => exact: Q1 | _ => fail end.
+match goal with |- is_true (R 1 P1 1 P11) => done | _ => fail end.
+Qed.
+
+Definition R1 := fun (x : nat) (p : P x) m (q : P (x+1)) (r : Q x p) => m > 0.
+
+Inductive myEx1 : Type :=
+ ExI1 : forall n (pn : P n) pn' (q : Q n pn), R1 n pn n pn' q -> myEx1.
+
+Hint Resolve (Q1 P1) : SSR.
+
+(* tests that goals in prop are solved in the right order, propagating instantiations,
+ thus the goal Q 1 ?p1 is faced by trivial after ?p1, and is thus evar free *)
+Lemma testmE14 : myEx1.
+Proof.
+apply: ExI1 1 _ _ _ _.
+match goal with |- is_true (R1 1 P1 1 P11 (Q1 P1)) => done | _ => fail end.
+Qed.
diff --git a/test-suite/ssr/abstract_var2.v b/test-suite/ssr/abstract_var2.v
new file mode 100644
index 000000000..7c57d2024
--- /dev/null
+++ b/test-suite/ssr/abstract_var2.v
@@ -0,0 +1,25 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssreflect.
+
+Set Implicit Arguments.
+
+Axiom P : nat -> nat -> Prop.
+
+Axiom tr :
+ forall x y z, P x y -> P y z -> P x z.
+
+Lemma test a b c : P a c -> P a b.
+Proof.
+intro H.
+Fail have [: s1 s2] H1 : P a b := @tr _ _ _ s1 s2.
+have [: w s1 s2] H1 : P a b := @tr _ w _ s1 s2.
+Abort.
diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v
new file mode 100644
index 000000000..97b7d830f
--- /dev/null
+++ b/test-suite/ssr/binders.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma test (x : bool) : True.
+have H1 x := x.
+have (x) := x => H2.
+have H3 T (x : T) := x.
+have ? : bool := H1 _ x.
+have ? : bool := H2 _ x.
+have ? : bool := H3 _ x.
+have ? (z : bool) : forall y : bool, z = z := fun y => refl_equal _.
+have ? w : w = w := @refl_equal nat w.
+have ? y : true by [].
+have ? (z : bool) : z = z.
+ exact: (@refl_equal _ z).
+have ? (z w : bool) : z = z by exact: (@refl_equal _ z).
+have H w (a := 3) (_ := 4) : w && true = w.
+ by rewrite andbT.
+exact I.
+Qed.
+
+Lemma test1 : True.
+suff (x : bool): x = x /\ True.
+ by move/(_ true); case=> _.
+split; first by exact: (@refl_equal _ x).
+suff H y : y && true = y /\ True.
+ by case: (H true).
+suff H1 /= : true && true /\ True.
+ by rewrite andbT; split; [exact: (@refl_equal _ y) | exact: I].
+match goal with |- is_true true /\ True => idtac end.
+by split.
+Qed.
+
+Lemma foo n : n >= 0.
+have f i (j := i + n) : j < n.
+ match goal with j := i + n |- _ => idtac end.
+Undo 2.
+suff f i (j := i + n) : j < n.
+ done.
+match goal with j := i + n |- _ => idtac end.
+Undo 3.
+done.
+Qed.
diff --git a/test-suite/ssr/binders_of.v b/test-suite/ssr/binders_of.v
new file mode 100644
index 000000000..69b52eace
--- /dev/null
+++ b/test-suite/ssr/binders_of.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+
+Require Import ssreflect.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : True.
+have f of seq nat & nat : nat.
+ exact 3.
+have g of nat := 3.
+have h of nat : nat := 3.
+have _ : f [::] 3 = g 3 + h 4.
+Admitted.
diff --git a/test-suite/ssr/caseview.v b/test-suite/ssr/caseview.v
new file mode 100644
index 000000000..94b064b02
--- /dev/null
+++ b/test-suite/ssr/caseview.v
@@ -0,0 +1,17 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Lemma test (A B : Prop) : A /\ B -> True.
+Proof. by case=> _ /id _. Qed.
diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v
new file mode 100644
index 000000000..7e60b04a6
--- /dev/null
+++ b/test-suite/ssr/congr.v
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall a b : nat, a == b -> a == 0 -> b == 0.
+Proof. move=> a b Eab Eac; congr (_ == 0) : Eac; exact: eqP Eab. Qed.
+
+Definition arrow A B := A -> B.
+
+Lemma test2 : forall a b : nat, a == b -> arrow (a == 0) (b == 0).
+Proof. move=> a b Eab; congr (_ == 0); exact: eqP Eab. Qed.
+
+Definition equals T (A B : T) := A = B.
+
+Lemma test3 : forall a b : nat, a = b -> equals nat (a + b) (b + b).
+Proof. move=> a b E; congr (_ + _); exact E. Qed.
+
+Variable S : eqType.
+Variable f : nat -> S.
+Coercion f : nat >-> Equality.sort.
+
+Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a).
+Proof. move=> a b Eba; congr (_ + _); exact: Eba. Qed.
diff --git a/test-suite/ssr/deferclear.v b/test-suite/ssr/deferclear.v
new file mode 100644
index 000000000..85353dadf
--- /dev/null
+++ b/test-suite/ssr/deferclear.v
@@ -0,0 +1,37 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Variable T : Type.
+
+Lemma test0 : forall a b c d : T, True.
+Proof. by move=> a b {a} a c; exact I. Qed.
+
+Variable P : T -> Prop.
+
+Lemma test1 : forall a b c : T, P a -> forall d : T, True.
+Proof. move=> a b {a} a _ d; exact I. Qed.
+
+Definition Q := forall x y : nat, x = y.
+Axiom L : 0 = 0 -> Q.
+Axiom L' : 0 = 0 -> forall x y : nat, x = y.
+Lemma test3 : Q.
+by apply/L.
+Undo.
+rewrite /Q.
+by apply/L.
+Undo 2.
+by apply/L'.
+Qed.
diff --git a/test-suite/ssr/dependent_type_err.v b/test-suite/ssr/dependent_type_err.v
new file mode 100644
index 000000000..a5789d8dd
--- /dev/null
+++ b/test-suite/ssr/dependent_type_err.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p.
+move=> n m p Hmn Hnp; rewrite -ltnS.
+Fail rewrite (_ : forall n0 m0 p0 : nat, m0 <= n0 -> n0 < p0 -> m0 < p0).
+Fail rewrite leq_ltn_trans.
+Admitted.
diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v
new file mode 100644
index 000000000..abf63a20c
--- /dev/null
+++ b/test-suite/ssr/derive_inversion.v
@@ -0,0 +1,29 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssreflect ssrbool.
+
+Set Implicit Arguments.
+
+ Inductive wf T : bool -> option T -> Type :=
+ | wf_f : wf false None
+ | wf_t : forall x, wf true (Some x).
+
+ Derive Inversion wf_inv with (forall T b (o : option T), wf b o) Sort Prop.
+
+ Lemma Problem T b (o : option T) :
+ wf b o ->
+ match b with
+ | true => exists x, o = Some x
+ | false => o = None
+ end.
+ Proof.
+ by case: b; elim/wf_inv=> //; case: o=> // a *; exists a.
+ Qed.
diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v
new file mode 100644
index 000000000..908249a36
--- /dev/null
+++ b/test-suite/ssr/elim.v
@@ -0,0 +1,279 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+(* Ltac debugging feature: recursive elim + eq generation *)
+Lemma testL1 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim branch: s => [|x xs _].
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
+Qed.
+
+(* The same but with explicit eliminator and a conflict in the intro pattern *)
+Lemma testL2 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim/last_ind branch: s => [|x s _].
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+match goal with _ : _ = rcons _ _ |- rcons _ _ = rcons _ _ => move: branch => // | _ => fail end.
+Qed.
+
+(* The same but without names for variables involved in the generated eq *)
+Lemma testL3 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; elim branch: s; move: (s) => _.
+match goal with _ : _ = [::] |- [::] = [::] => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ = _ :: _ |- _ :: _ = _ :: _ => move: branch => // | _ => fail end.
+Qed.
+
+Inductive foo : Type := K1 : foo | K2 : foo -> foo -> foo | K3 : (nat -> foo) -> foo.
+
+(* The same but with more intros to be done *)
+Lemma testL4 : forall (o : foo), o = o.
+Proof.
+move=> o; elim branch: o.
+match goal with _ : _ = K1 |- K1 = K1 => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ = K2 _ _ |- K2 _ _ = K2 _ _ => move: branch => // | _ => fail end.
+move=> _; match goal with _ : _ = K3 _ |- K3 _ = K3 _ => move: branch => // | _ => fail end.
+Qed.
+
+(* Occurrence counting *)
+Lemma testO1: forall (b : bool), b = b.
+Proof.
+move=> b; case: (b) / idP.
+match goal with |- is_true b -> true = true => done | _ => fail end.
+match goal with |- ~ is_true b -> false = false => done | _ => fail end.
+Qed.
+
+(* The same but only the second occ *)
+Lemma testO2: forall (b : bool), b = b.
+Proof.
+move=> b; case: {2}(b) / idP.
+match goal with |- is_true b -> b = true => done | _ => fail end.
+match goal with |- ~ is_true b -> b = false => move/(introF idP) => // | _ => fail end.
+Qed.
+
+(* The same but with eq generation *)
+Lemma testO3: forall (b : bool), b = b.
+Proof.
+move=> b; case E: {2}(b) / idP.
+match goal with _ : is_true b, _ : b = true |- b = true => move: E => _; done | _ => fail end.
+match goal with H : ~ is_true b, _ : b = false |- b = false => move: E => _; move/(introF idP): H => // | _ => fail end.
+Qed.
+
+(* Views *)
+Lemma testV1 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP E: {1}s => [| x xs].
+match goal with _ : s = [::] |- [::] = s => symmetry; exact E | _ => fail end.
+match goal with _ : s = rcons x xs |- rcons _ _ = s => symmetry; exact E | _ => fail end.
+Qed.
+
+Lemma testV2 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP E: s => [| x xs].
+match goal with _ : s = [::] |- [::] = [::] => done | _ => fail end.
+match goal with _ : s = rcons x xs |- rcons _ _ = rcons _ _ => done | _ => fail end.
+Qed.
+
+Lemma testV3 : forall A (s : seq A), s = s.
+Proof.
+move=> A s; case/lastP: s => [| x xs].
+match goal with |- [::] = [::] => done | _ => fail end.
+match goal with |- rcons _ _ = rcons _ _ => done | _ => fail end.
+Qed.
+
+(* Patterns *)
+Lemma testP1: forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim: {2}(_ == _) / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
+Qed.
+
+(* The same but with an implicit pattern *)
+Lemma testP2 : forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim: {2}_ / eqP.
+match goal with |- (y = x -> is_true ((y == x) && true) -> is_true (y == x)) => move=> -> // | _ => fail end.
+match goal with |- (y <> x -> is_true ((y == x) && false) -> is_true (y == x)) => move=> _; rewrite andbC // | _ => fail end.
+Qed.
+
+(* The same but with an eq generation switch *)
+Lemma testP3 : forall (x y : nat), (y == x) && (y == x) -> y == x.
+move=> x y; elim E: {2}_ / eqP.
+match goal with _ : y = x |- (is_true ((y == x) && true) -> is_true (y == x)) => rewrite E; reflexivity | _ => fail end.
+match goal with _ : y <> x |- (is_true ((y == x) && false) -> is_true (y == x)) => rewrite E => /= H; exact H | _ => fail end.
+Qed.
+
+Inductive spec : nat -> nat -> nat -> Prop :=
+| specK : forall a b c, a = 0 -> b = 2 -> c = 4 -> spec a b c.
+Lemma specP : spec 0 2 4. Proof. by constructor. Qed.
+
+Lemma testP4 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: specP => a b c defa defb defc.
+match goal with |- (a.+1 + a.+1) * c = b + (a.+1 + a.+1) + (b + b) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP5 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: (1 + 1) _ / specP => a b c defa defb defc.
+match goal with |- b * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP6 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: {2}(1 + 1) _ / specP => a b c defa defb defc.
+match goal with |- (a.+1 + a.+1) * c = a.+2 + b + (a.+2 + a.+2) => subst; done | _ => fail end.
+Qed.
+
+Lemma testP7 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case: _ (1 + 1) (2 + _) / specP => a b c defa defb defc.
+match goal with |- b * a.+4 = c + c => subst; done | _ => fail end.
+Qed.
+
+Lemma testP8 : (1+1) * 4 = 2 + (1+1) + (2 + 2).
+Proof.
+case E: (1 + 1) (2 + _) / specP=> [a b c defa defb defc].
+match goal with |- b * a.+4 = c + c => subst; done | _ => fail end.
+Qed.
+
+Variables (T : Type) (tr : T -> T).
+
+Inductive exec (cf0 cf1 : T) : seq T -> Prop :=
+| exec_step : tr cf0 = cf1 -> exec cf0 cf1 [::]
+| exec_star : forall cf2 t, tr cf0 = cf2 ->
+ exec cf2 cf1 t -> exec cf0 cf1 (cf2 :: t).
+
+Inductive execr (cf0 cf1 : T) : seq T -> Prop :=
+| execr_step : tr cf0 = cf1 -> execr cf0 cf1 [::]
+| execr_star : forall cf2 t, execr cf0 cf2 t ->
+ tr cf2 = cf1 -> execr cf0 cf1 (t ++ [:: cf2]).
+
+Lemma execP : forall cf0 cf1 t, exec cf0 cf1 t <-> execr cf0 cf1 t.
+Proof.
+move=> cf0 cf1 t; split => [] Ecf.
+ elim: Ecf.
+ match goal with |- forall cf2 cf3 : T, tr cf2 = cf3 ->
+ execr cf2 cf3 [::] => myadmit | _ => fail end.
+ match goal with |- forall (cf2 cf3 cf4 : T) (t0 : seq T),
+ tr cf2 = cf4 -> exec cf4 cf3 t0 -> execr cf4 cf3 t0 ->
+ execr cf2 cf3 (cf4 :: t0) => myadmit | _ => fail end.
+elim: Ecf.
+ match goal with |- forall cf2 : T,
+ tr cf0 = cf2 -> exec cf0 cf2 [::] => myadmit | _ => fail end.
+match goal with |- forall (cf2 cf3 : T) (t0 : seq T),
+ execr cf0 cf3 t0 -> exec cf0 cf3 t0 -> tr cf3 = cf2 ->
+ exec cf0 cf2 (t0 ++ [:: cf3]) => myadmit | _ => fail end.
+Qed.
+
+Fixpoint plus (m n : nat) {struct n} : nat :=
+ match n with
+ | 0 => m
+ | S p => S (plus m p)
+ end.
+
+Definition plus_equation :
+forall m n : nat,
+ plus m n =
+ match n with
+ | 0 => m
+ | p.+1 => (plus m p).+1
+ end
+:=
+fun m n : nat =>
+match
+ n as n0
+ return
+ (forall m0 : nat,
+ plus m0 n0 =
+ match n0 with
+ | 0 => m0
+ | p.+1 => (plus m0 p).+1
+ end)
+with
+| 0 => @erefl nat
+| n0.+1 => fun m0 : nat => erefl (plus m0 n0).+1
+end m.
+
+Definition plus_rect :
+forall (m : nat) (P : nat -> nat -> Type),
+ (forall n : nat, n = 0 -> P 0 m) ->
+ (forall n p : nat,
+ n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
+ forall n : nat, P n (plus m n)
+:=
+fun (m : nat) (P : nat -> nat -> Type)
+ (f0 : forall n : nat, n = 0 -> P 0 m)
+ (f : forall n p : nat,
+ n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) =>
+fix plus0 (n : nat) : P n (plus m n) :=
+ eq_rect_r [eta P n]
+ (let f1 := f0 n in
+ let f2 := f n in
+ match
+ n as n0
+ return
+ (n = n0 ->
+ (forall p : nat,
+ n0 = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
+ (n0 = 0 -> P 0 m) ->
+ P n0 match n0 with
+ | 0 => m
+ | p.+1 => (plus m p).+1
+ end)
+ with
+ | 0 =>
+ fun (_ : n = 0)
+ (_ : forall p : nat,
+ 0 = p.+1 ->
+ P p (plus m p) -> P p.+1 (plus m p).+1)
+ (f4 : 0 = 0 -> P 0 m) => unkeyed (f4 (erefl 0))
+ | n0.+1 =>
+ fun (_ : n = n0.+1)
+ (f3 : forall p : nat,
+ n0.+1 = p.+1 ->
+ P p (plus m p) -> P p.+1 (plus m p).+1)
+ (_ : n0.+1 = 0 -> P 0 m) =>
+ let f5 :=
+ let p := n0 in
+ let H := erefl n0.+1 : n0.+1 = p.+1 in f3 p H in
+ unkeyed (let Hrec := plus0 n0 in f5 Hrec)
+ end (erefl n) f2 f1) (plus_equation m n).
+
+Definition plus_ind := plus_rect.
+
+Lemma exF x y z: plus (plus x y) z = plus x (plus y z).
+elim/plus_ind: z / (plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: (plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: {z}(plus _ z).
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: {z}_.
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+Undo 2.
+elim/plus_ind: z / _.
+match goal with |- forall n : nat, n = 0 -> plus x y = plus x (plus y 0) => idtac end.
+ done.
+by move=> _ p _ ->.
+Qed.
+
+(* BUG elim-False *)
+Lemma testeF : False -> 1 = 0.
+Proof. by elim. Qed.
diff --git a/test-suite/ssr/elim2.v b/test-suite/ssr/elim2.v
new file mode 100644
index 000000000..c7c20d8f8
--- /dev/null
+++ b/test-suite/ssr/elim2.v
@@ -0,0 +1,74 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+(* div fintype finfun path bigop. *)
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
+ let s := \big[op/idx]_(i <- r | P i) F i in
+ K s * K' s -> K' s.
+Proof. by move=> /= [_]. Qed.
+Arguments big_load [R] K [K' idx op I r P F].
+
+Section Elim1.
+
+Variables (R : Type) (K : R -> Type) (f : R -> R).
+Variables (idx : R) (op op' : R -> R -> R).
+
+Hypothesis Kid : K idx.
+
+Ltac ASSERT1 := match goal with |- (K idx) => myadmit end.
+Ltac ASSERT2 K := match goal with |- (forall x1 : R, R ->
+ forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end.
+
+
+Lemma big_rec I r (P : pred I) F
+ (Kop : forall i x, P i -> K x -> K (op (F i) x)) :
+ K (\big[op/idx]_(i <- r | P i) F i).
+Proof.
+elim/big_ind2: {-}_.
+ ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
+elim/big_ind2: _ / {-}_.
+ ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
+
+elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i))
+ / (\big[op/idx]_(i <- r | P i) F i).
+ ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3.
+
+elim/(big_load (phantom R)): _.
+ Undo.
+
+Fail elim/big_rec2: {2}_.
+
+elim/big_rec2: (\big[op/idx]_(i <- r | P i) F i)
+ / {1}(\big[op/idx]_(i <- r | P i) F i).
+ Undo.
+
+elim/(big_load (phantom R)): _.
+Undo.
+
+Fail elim/big_rec2: _ / {2}(\big[op/idx]_(i <- r | P i) F i).
+Admitted.
+
+Definition morecomplexthannecessary A (P : A -> A -> Prop) x y := P x y.
+
+Lemma grab A (P : A -> A -> Prop) n m : (n = m) -> (P n n) -> morecomplexthannecessary A P n m.
+by move->.
+Qed.
+
+Goal forall n m, m + (n + m) = m + (n * 1 + m).
+Proof. move=> n m; elim/grab : (_ * _) / {1}n => //; exact: muln1. Qed.
+
+End Elim1.
diff --git a/test-suite/ssr/elim_pattern.v b/test-suite/ssr/elim_pattern.v
new file mode 100644
index 000000000..ef4658287
--- /dev/null
+++ b/test-suite/ssr/elim_pattern.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1).
+case: (X in _ = X) / eqP => _.
+match goal with |- (x == x) = true => myadmit end.
+match goal with |- (x == x) = false => myadmit end.
+Qed.
+
+Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1).
+elim: (x in RHS).
+match goal with |- (x == x) = _ => myadmit end.
+match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end.
+Qed.
diff --git a/test-suite/ssr/first_n.v b/test-suite/ssr/first_n.v
new file mode 100644
index 000000000..4971add91
--- /dev/null
+++ b/test-suite/ssr/first_n.v
@@ -0,0 +1,21 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test : False -> (bool -> False -> True -> True) -> True.
+move=> F; let w := constr:(2) in apply; last w first.
+- by apply: F.
+- by apply: I.
+- by apply: true.
+Qed.
diff --git a/test-suite/ssr/gen_have.v b/test-suite/ssr/gen_have.v
new file mode 100644
index 000000000..249e006f9
--- /dev/null
+++ b/test-suite/ssr/gen_have.v
@@ -0,0 +1,174 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Axiom P : nat -> Prop.
+Lemma clear_test (b1 b2 : bool) : b2 = b2.
+Proof.
+(* wlog gH : (b3 := b2) / b2 = b3. myadmit. *)
+gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3.
+ myadmit.
+Fail exact (H b1).
+exact (H b2 (erefl _)).
+Qed.
+
+
+Lemma test1 n (ngt0 : 0 < n) : P n.
+gen have lt2le, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
+ match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+Check (H1 : 0 <= n).
+Check (H2 : n != 0).
+myadmit.
+Qed.
+
+Lemma test2 n (ngt0 : 0 < n) : P n.
+gen have _, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
+ match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+lazymatch goal with
+ | lt2le : forall n : nat, is_true(0 < n) -> is_true((0 <= n) && (n != 0))
+ |- _ => fail "not cleared"
+ | _ => idtac end.
+Check (H1 : 0 <= n).
+Check (H2 : n != 0).
+myadmit.
+Qed.
+
+Lemma test3 n (ngt0 : 0 < n) : P n.
+gen have H : n ngt0 / (0 <= n) && (n != 0).
+ match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test4 n (ngt0 : 0 < n) : P n.
+gen have : n ngt0 / (0 <= n) && (n != 0).
+ match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+move=> H.
+Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test4bis n (ngt0 : 0 < n) : P n.
+wlog suff : n ngt0 / (0 <= n) && (n != 0); last first.
+ match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
+move=> H.
+Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test5 n (ngt0 : 0 < n) : P n.
+Fail gen have : / (0 <= n) && (n != 0).
+Abort.
+
+Lemma test6 n (ngt0 : 0 < n) : P n.
+gen have : n ngt0 / (0 <= n) && (n != 0) by myadmit.
+Abort.
+
+Lemma test7 n (ngt0 : 0 < n) : P n.
+Fail gen have : n / (0 <= n) && (n != 0).
+Abort.
+
+Lemma test3wlog2 n (ngt0 : 0 < n) : P n.
+gen have H : (m := n) ngt0 / (0 <= m) && (m != 0).
+ match goal with
+ ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => myadmit end.
+Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
+myadmit.
+Qed.
+
+Lemma test3wlog3 n (ngt0 : 0 < n) : P n.
+gen have H : {n} (m := n) (n := 0) ngt0 / (0 <= m) && (m != n).
+ match goal with
+ ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => myadmit end.
+Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)).
+myadmit.
+Qed.
+
+Lemma testw1 n (ngt0 : 0 < n) : n <= 0.
+wlog H : (z := 0) (m := n) ngt0 / m != 0.
+ match goal with
+ |- (forall z m,
+ is_true(z < m) -> is_true(m != 0) -> is_true(m <= z)) ->
+ is_true(n <= 0) => myadmit end.
+Check(n : nat).
+Check(m : nat).
+Check(z : nat).
+Check(ngt0 : z < m).
+Check(H : m != 0).
+myadmit.
+Qed.
+
+Lemma testw2 n (ngt0 : 0 < n) : n <= 0.
+wlog H : (m := n) (z := (X in n <= X)) ngt0 / m != z.
+ match goal with
+ |- (forall m z : nat,
+ is_true(0 < m) -> is_true(m != z) -> is_true(m <= z)) ->
+ is_true(n <= 0) => idtac end.
+Restart.
+wlog H : (m := n) (one := (X in X <= _)) ngt0 / m != one.
+ match goal with
+ |- (forall m one : nat,
+ is_true(one <= m) -> is_true(m != one) -> is_true(m <= 0)) ->
+ is_true(n <= 0) => idtac end.
+Restart.
+wlog H : {n} (m := n) (z := (X in _ <= X)) ngt0 / m != z.
+ match goal with
+ |- (forall m z : nat,
+ is_true(0 < z) -> is_true(m != z) -> is_true(m <= 0)) ->
+ is_true(n <= 0) => idtac end.
+ myadmit.
+Fail Check n.
+myadmit.
+Qed.
+
+Section Test.
+Variable x : nat.
+Definition addx y := y + x.
+
+Lemma testw3 (m n : nat) (ngt0 : 0 < n) : n <= addx x.
+wlog H : (n0 := n) (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
+ myadmit.
+myadmit.
+Qed.
+
+
+Definition twox := x + x.
+Definition bis := twox.
+
+Lemma testw3x n (ngt0 : 0 < n) : n + x <= twox.
+wlog H : (y := x) (@twoy := (X in _ <= X)) / twoy = 2 * y.
+ match goal with
+ |- (forall y : nat,
+ let twoy := y + y in
+ twoy = 2 * y -> is_true(n + y <= twoy)) ->
+ is_true(n + x <= twox) => myadmit end.
+Restart.
+wlog H : (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
+ match goal with
+ |- (forall y : nat,
+ let twoy := twox in
+ twoy = 2 * y -> is_true(n + y <= twoy)) ->
+ is_true(n + x <= twox) => myadmit end.
+myadmit.
+Qed.
+
+End Test.
+
+Lemma test_in n k (def_k : k = 0) (ngtk : k < n) : P n.
+rewrite -(add0n n) in {def_k k ngtk} (m := k) (def_m := def_k) (ngtm := ngtk).
+rewrite def_m add0n in {ngtm} (e := erefl 0 ) (ngt0 := ngtm) => {def_m}.
+myadmit.
+Qed.
diff --git a/test-suite/ssr/gen_pattern.v b/test-suite/ssr/gen_pattern.v
new file mode 100644
index 000000000..c0592e884
--- /dev/null
+++ b/test-suite/ssr/gen_pattern.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Notation "( a 'in' c )" := (a + c) (only parsing) : myscope.
+Delimit Scope myscope with myscope.
+
+Notation "( a 'in' c )" := (a + c) (only parsing).
+
+Lemma foo x y : x + x.+1 = x.+1 + y.
+move: {x} (x.+1) {1}x y (x.+1 in RHS).
+ match goal with |- forall a b c d, b + a = d + c => idtac end.
+Admitted.
+
+Lemma bar x y : x + x.+1 = x.+1 + y.
+move E: ((x.+1 in y)) => w.
+ match goal with |- x + x.+1 = w => rewrite -{w}E end.
+move E: (x.+1 in y)%myscope => w.
+ match goal with |- x + x.+1 = w => rewrite -{w}E end.
+move E: ((x + y).+1 as RHS) => w.
+ match goal with |- x + x.+1 = w => rewrite -{}E -addSn end.
+Admitted.
diff --git a/test-suite/ssr/have_TC.v b/test-suite/ssr/have_TC.v
new file mode 100644
index 000000000..b3a26ed2c
--- /dev/null
+++ b/test-suite/ssr/have_TC.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Class foo (T : Type) := { n : nat }.
+Instance five : foo nat := {| n := 5 |}.
+
+Definition bar T {f : foo T} m : Prop :=
+ @n _ f = m.
+
+Eval compute in (bar nat 7).
+
+Lemma a : True.
+set toto := bar _ 8.
+have titi : bar _ 5.
+ reflexivity.
+have titi2 : bar _ 5 := .
+ Fail reflexivity.
+ by myadmit.
+have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
+move/totoc: nat => _.
+exact I.
+Qed.
+
+Set SsrHave NoTCResolution.
+
+Lemma a' : True.
+set toto := bar _ 8.
+have titi : bar _ 5.
+ Fail reflexivity.
+ by myadmit.
+have titi2 : bar _ 5 := .
+ Fail reflexivity.
+ by myadmit.
+have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
+move/totoc: nat => _.
+exact I.
+Qed.
diff --git a/test-suite/ssr/have_transp.v b/test-suite/ssr/have_transp.v
new file mode 100644
index 000000000..1c998da71
--- /dev/null
+++ b/test-suite/ssr/have_transp.v
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+
+Lemma test1 n : n >= 0.
+Proof.
+have [:s1] @h m : 'I_(n+m).+1.
+ apply: Sub 0 _.
+ abstract: s1 m.
+ by auto.
+cut (forall m, 0 < (n+m).+1); last assumption.
+rewrite [_ 1 _]/= in s1 h *.
+by [].
+Qed.
+
+Lemma test2 n : n >= 0.
+Proof.
+have [:s1] @h m : 'I_(n+m).+1 := Sub 0 (s1 m).
+ move=> m; reflexivity.
+cut (forall m, 0 < (n+m).+1); last assumption.
+by [].
+Qed.
+
+Lemma test3 n : n >= 0.
+Proof.
+Fail have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0 (s1 m)); auto.
+have [:s1] @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract: s1 m; auto.
+cut (forall m, 0 < (n+m).+1); last assumption.
+by [].
+Qed.
+
+Lemma test4 n : n >= 0.
+Proof.
+have @h m : 'I_(n+m).+1 by apply: (Sub 0); abstract auto.
+by [].
+Qed.
diff --git a/test-suite/ssr/have_view_idiom.v b/test-suite/ssr/have_view_idiom.v
new file mode 100644
index 000000000..3d6c9d980
--- /dev/null
+++ b/test-suite/ssr/have_view_idiom.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test (a b : bool) (pab : a && b) : b.
+have {pab} /= /andP [pa -> //] /= : true && (a && b) := pab.
+Qed.
diff --git a/test-suite/ssr/havesuff.v b/test-suite/ssr/havesuff.v
new file mode 100644
index 000000000..aa1f71879
--- /dev/null
+++ b/test-suite/ssr/havesuff.v
@@ -0,0 +1,85 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Variables P G : Prop.
+
+Lemma test1 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H : P.
+ match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test2 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suffices {pg} H : P.
+ match goal with |- P -> G => move=> _; exact: pg p | _ => fail end.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test3 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H : P.
+ match goal with H : P |- G => exact: pg H | _ => fail end.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+
+Lemma test4 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suffices have {pg} H: P.
+ match goal with H : P |- G => exact: pg H | _ => fail end.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+
+(*
+Lemma test5 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H : P := pg H.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+*)
+
+(*
+Lemma test6 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+suff have {pg} H := pg H.
+match goal with |- (P -> G) -> G => move=> H; exact: H p | _ => fail end.
+Qed.
+*)
+
+Lemma test7 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H : P := pg.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Lemma test8 : (P -> G) -> P -> G.
+Proof.
+move=> pg p.
+have suff {pg} H := pg.
+match goal with H : P -> G |- G => exact: H p | _ => fail end.
+Qed.
+
+Goal forall x y : bool, x = y -> x = y.
+move=> x y E.
+by have {x E} -> : x = y by [].
+Qed.
diff --git a/test-suite/ssr/if_isnt.v b/test-suite/ssr/if_isnt.v
new file mode 100644
index 000000000..b8f6b7739
--- /dev/null
+++ b/test-suite/ssr/if_isnt.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Definition unopt (x : option bool) :=
+ if x isn't Some x then false else x.
+
+Lemma test1 : unopt None = false /\
+ unopt (Some false) = false /\
+ unopt (Some true) = true.
+Proof. by auto. Qed.
diff --git a/test-suite/ssr/intro_beta.v b/test-suite/ssr/intro_beta.v
new file mode 100644
index 000000000..8a164bd80
--- /dev/null
+++ b/test-suite/ssr/intro_beta.v
@@ -0,0 +1,25 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Axiom T : Type.
+
+Definition C (P : T -> Prop) := forall x, P x.
+
+Axiom P : T -> T -> Prop.
+
+Lemma foo : C (fun x => forall y, let z := x in P y x).
+move=> a b.
+match goal with |- (let y := _ in _) => idtac end.
+Admitted.
diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v
new file mode 100644
index 000000000..fdc85173a
--- /dev/null
+++ b/test-suite/ssr/intro_noop.v
@@ -0,0 +1,37 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Lemma v : True -> bool -> bool. Proof. by []. Qed.
+
+Reserved Notation " a -/ b " (at level 0).
+Reserved Notation " a -// b " (at level 0).
+Reserved Notation " a -/= b " (at level 0).
+Reserved Notation " a -//= b " (at level 0).
+
+Lemma test : forall a b c, a || b || c.
+Proof.
+move=> ---a--- - -/=- -//- -/=- -//=- b [|-].
+move: {-}a => /v/v-H; have _ := H I I.
+Fail move: {-}a {H} => /v-/v-H.
+have - -> : a = (id a) by [].
+have --> : a = (id a) by [].
+have - - _ : a = (id a) by [].
+have -{1}-> : a = (id a) by [].
+ by myadmit.
+move: a.
+case: b => -[] //.
+by myadmit.
+Qed.
diff --git a/test-suite/ssr/ipatalternation.v b/test-suite/ssr/ipatalternation.v
new file mode 100644
index 000000000..6aa9a954c
--- /dev/null
+++ b/test-suite/ssr/ipatalternation.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True.
+by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right.
+Qed.
diff --git a/test-suite/ssr/ltac_have.v b/test-suite/ssr/ltac_have.v
new file mode 100644
index 000000000..380e52af4
--- /dev/null
+++ b/test-suite/ssr/ltac_have.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Ltac SUFF1 h t := suff h x (p := x < 0) : t.
+Ltac SUFF2 h t := suff h x (p := x < 0) : t by apply h.
+Ltac HAVE1 h t u := have h x (p := x < 0) : t := u.
+Ltac HAVE2 h t := have h x (p := x < 0) : t by [].
+Ltac HAVE3 h t := have h x (p := x < 0) : t.
+Ltac HAVES h t := have suff h : t.
+Ltac SUFFH h t := suff have h : t.
+
+Lemma foo z : z < 0.
+SUFF1 h1 (z+1 < 0).
+Undo.
+SUFF2 h2 (z < 0).
+Undo.
+HAVE1 h3 (z = z) (refl_equal z).
+Undo.
+HAVE2 h4 (z = z).
+Undo.
+HAVE3 h5 (z < 0).
+Undo.
+HAVES h6 (z < 1).
+Undo.
+SUFFH h7 (z < 1).
+Undo.
+Admitted.
diff --git a/test-suite/ssr/ltac_in.v b/test-suite/ssr/ltac_in.v
new file mode 100644
index 000000000..bcdf96dde
--- /dev/null
+++ b/test-suite/ssr/ltac_in.v
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+(* error 1 *)
+
+Ltac subst1 H := move: H; rewrite {1} addnC; move => H.
+Ltac subst2 H := rewrite addnC in H.
+
+Goal ( forall a b: nat, b+a = 0 -> b+a=0).
+Proof. move=> a b hyp. subst1 hyp. subst2 hyp. done. Qed.
diff --git a/test-suite/ssr/move_after.v b/test-suite/ssr/move_after.v
new file mode 100644
index 000000000..a7a9afea0
--- /dev/null
+++ b/test-suite/ssr/move_after.v
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Goal True -> True -> True.
+move=> H1 H2.
+move H1 after H2.
+Admitted.
diff --git a/test-suite/ssr/multiview.v b/test-suite/ssr/multiview.v
new file mode 100644
index 000000000..f4e717b38
--- /dev/null
+++ b/test-suite/ssr/multiview.v
@@ -0,0 +1,58 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Goal forall m n p, n <= p -> m <= n -> m <= p.
+by move=> m n p le_n_p /leq_trans; apply.
+Undo 1.
+by move=> m n p le_n_p /leq_trans /(_ le_n_p) le_m_p; exact: le_m_p.
+Undo 1.
+by move=> m n p le_n_p /leq_trans ->.
+Qed.
+
+Goal forall P Q X : Prop, Q -> (True -> X -> Q = P) -> X -> P.
+by move=> P Q X q V /V <-.
+Qed.
+
+Lemma test0: forall a b, a && a && b -> b.
+by move=> a b; repeat move=> /andP []; move=> *.
+Qed.
+
+Lemma test1 : forall a b, a && b -> b.
+by move=> a b /andP /andP /andP [] //.
+Qed.
+
+Lemma test2 : forall a b, a && b -> b.
+by move=> a b /andP /andP /(@andP a) [] //.
+Qed.
+
+Lemma test3 : forall a b, a && (b && b) -> b.
+by move=> a b /andP [_ /andP [_ //]].
+Qed.
+
+Lemma test4: forall a b, a && b = b && a.
+by move=> a b; apply/andP/andP=> ?; apply/andP/andP/andP; rewrite andbC; apply/andP.
+Qed.
+
+Lemma test5: forall C I A O, (True -> O) -> (O -> A) -> (True -> A -> I) -> (I -> C) -> C.
+by move=> c i a o O A I C; apply/C/I/A/O.
+Qed.
+
+Lemma test6: forall A B, (A -> B) -> A -> B.
+move=> A B A_to_B a; move/A_to_B in a; exact: a.
+Qed.
+
+Lemma test7: forall A B, (A -> B) -> A -> B.
+move=> A B A_to_B a; apply A_to_B in a; exact: a.
+Qed.
diff --git a/test-suite/ssr/occarrow.v b/test-suite/ssr/occarrow.v
new file mode 100644
index 000000000..49af7ae08
--- /dev/null
+++ b/test-suite/ssr/occarrow.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n.
+move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-.
+by move: E => {3}->.
+Qed.
+
+Lemma test2 : forall n m : nat, True /\ (n = m -> n * n = n * m).
+by move=> n m; constructor=> [|{2}->].
+Qed.
diff --git a/test-suite/ssr/patnoX.v b/test-suite/ssr/patnoX.v
new file mode 100644
index 000000000..d69f03ac3
--- /dev/null
+++ b/test-suite/ssr/patnoX.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Goal forall x, x && true = x.
+move=> x.
+Fail (rewrite [X in _ && _]andbT).
+Abort.
diff --git a/test-suite/ssr/pattern.v b/test-suite/ssr/pattern.v
new file mode 100644
index 000000000..396f4f032
--- /dev/null
+++ b/test-suite/ssr/pattern.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssrmatching.
+
+(*Set Debug SsrMatching.*)
+
+Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) :=
+ let name := fresh in
+ let def_name := fresh in
+ ssrpattern pat;
+ intro name;
+ pose proof (refl_equal name) as def_name;
+ unfold name at 1 in def_name;
+ t def_name;
+ [ rewrite <- def_name | idtac.. ];
+ clear name def_name.
+
+Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4.
+Proof.
+at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place).
+- reflexivity.
+- trivial.
+- trivial.
+Qed.
diff --git a/test-suite/ssr/primproj.v b/test-suite/ssr/primproj.v
new file mode 100644
index 000000000..cf61eb436
--- /dev/null
+++ b/test-suite/ssr/primproj.v
@@ -0,0 +1,164 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+
+
+Require Import Setoid.
+Set Primitive Projections.
+
+
+Module CoqBug.
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+(* Coq equally fails *)
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Set Keyed Unification.
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Admitted.
+
+End CoqBug.
+
+(* ----------------------------------------------- *)
+Require Import ssreflect.
+
+Set Primitive Projections.
+
+Module T1.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Goal foo_car _ bar = 10.
+Proof.
+match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+rewrite /foo_car.
+(*
+Fail match goal with
+| |- foo_car _ bar = 10 => idtac
+end.
+*)
+Admitted.
+
+End T1.
+
+
+Module T2.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+match goal with
+| |- foo_car bar = 10 => idtac
+end.
+rewrite /foo_car.
+(*
+Fail match goal with
+| |- foo_car bar = 10 => idtac
+end.
+*)
+Admitted.
+
+End T2.
+
+
+Module T3.
+
+Record foo {A} := Foo { foo_car : A }.
+
+Definition bar : foo := Foo nat 10.
+
+Goal foo_car bar = 10.
+Proof.
+rewrite -[foo_car _]/(id _).
+match goal with |- id _ = 10 => idtac end.
+Admitted.
+
+Goal foo_car bar = 10.
+Proof.
+set x := foo_car _.
+match goal with |- x = 10 => idtac end.
+Admitted.
+
+End T3.
+
+Module T4.
+
+Inductive seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Arguments unseal {_ _} _.
+Arguments seal_eq {_ _} _.
+
+Record uPred : Type := IProp { uPred_holds :> Prop }.
+
+Definition uPred_or_def (P Q : uPred) : uPred :=
+ {| uPred_holds := P \/ Q |}.
+Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed.
+Definition uPred_or := unseal uPred_or_aux.
+Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux.
+
+Lemma foobar (P1 P2 Q : uPred) :
+ (P1 <-> P2) -> (uPred_or P1 Q) <-> (uPred_or P2 Q).
+Proof.
+ rewrite uPred_or_eq. (* This fails. *)
+Admitted.
+
+End T4.
+
+
+Module DesignFlaw.
+
+Record foo A := Foo { foo_car : A }.
+Definition bar : foo _ := Foo nat 10.
+
+Definition app (f : foo nat -> nat) x := f x.
+
+Goal app (foo_car _) bar = 10.
+Proof.
+unfold app. (* mkApp should produce a Proj *)
+Fail set x := (foo_car _ _).
+Admitted.
+
+End DesignFlaw.
+
+
+Module Bug.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+Fail rewrite e. (* Issue: #86 *)
+Admitted.
+
+End Bug.
diff --git a/test-suite/ssr/rewpatterns.v b/test-suite/ssr/rewpatterns.v
new file mode 100644
index 000000000..f7993f402
--- /dev/null
+++ b/test-suite/ssr/rewpatterns.v
@@ -0,0 +1,146 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun TestSuite.ssr_mini_mathcomp.
+
+Lemma test1 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1).
+by move=> x y f; rewrite [_.+1](addnC x.+1).
+Qed.
+
+Lemma test2 : forall x y f, x + y + f (y + x) + f (y + x) = x + y + f (y + x) + f (x + y).
+by move=> x y f; rewrite {2}[in f _]addnC.
+Qed.
+
+Lemma test2' : forall x y f, true && f (x * (y + x)) = true && f(x * (x + y)).
+by move=> x y f; rewrite [in f _](addnC y).
+Qed.
+
+Lemma test2'' : forall x y f, f (y + x) + f(y + x) + f(y + x) = f(x + y) + f(y + x) + f(x + y).
+by move=> x y f; rewrite {1 3}[in f _](addnC y).
+Qed.
+
+(* patterns catching bound vars not supported *)
+Lemma test2_1 : forall x y f, true && (let z := x in f (z * (y + x))) = true && f(x * (x + y)).
+by move=> x y f; rewrite [in f _](addnC x). (* put y when bound var will be OK *)
+Qed.
+
+Lemma test3 : forall x y f, x + f (x + y) (f (y + x) x) = x + f (x + y) (f (x + y) x).
+by move=> x y f; rewrite [in X in (f _ X)](addnC y).
+Qed.
+
+Lemma test3' : forall x y f, x = y -> x + f (x + x) x + f (x + x) x =
+ x + f (x + y) x + f (y + x) x.
+by move=> x y f E; rewrite {2 3}[in X in (f X _)]E.
+Qed.
+
+Lemma test3'' : forall x y f, x = y -> x + f (x + y) x + f (x + y) x =
+ x + f (x + y) x + f (y + y) x.
+by move=> x y f E; rewrite {2}[in X in (f X _)]E.
+Qed.
+
+Lemma test4 : forall x y f, x = y -> x + f (fun _ : nat => x + x) x + f (fun _ => x + x) x =
+ x + f (fun _ => x + y) x + f (fun _ => y + x) x.
+by move=> x y f E; rewrite {2 3}[in X in (f X _)]E.
+Qed.
+
+Lemma test4' : forall x y f, x = y -> x + f (fun _ _ _ : nat => x + x) x =
+ x + f (fun _ _ _ => x + y) x.
+by move=> x y f E; rewrite {2}[in X in (f X _)]E.
+Qed.
+
+Lemma test5 : forall x y f, x = y -> x + f (y + x) x + f (y + x) x =
+ x + f (x + y) x + f (y + x) x.
+by move=> x y f E; rewrite {1}[X in (f X _)]addnC.
+Qed.
+
+Lemma test3''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) =
+ x + f (x + y) x + f (y + y) (x + y).
+by move=> x y f E; rewrite {1}[in X in (f X X)]E.
+Qed.
+
+Lemma test3'''' : forall x y f, x = y -> x + f (x + y) x + f (x + y) (x + y) =
+ x + f (x + y) x + f (y + y) (y + y).
+by move=> x y f E; rewrite [in X in (f X X)]E.
+Qed.
+
+Lemma test3x : forall x y f, y+y = x+y -> x + f (x + y) x + f (x + y) (x + y) =
+ x + f (x + y) x + f (y + y) (y + y).
+by move=> x y f E; rewrite -[X in (f X X)]E.
+Qed.
+
+Lemma test6 : forall x y (f : nat -> nat), f (x + y).+1 = f (y.+1 + x).
+by move=> x y f; rewrite [(x + y) in X in (f X)]addnC.
+Qed.
+
+Lemma test7 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1).
+by move=> x y f; rewrite [(x.+1 + y) as X in (f X)]addnC.
+Qed.
+
+Lemma manual x y z (f : nat -> nat -> nat) : (x + y).+1 + f (x.+1 + y) (z + (x + y).+1) = 0.
+Proof.
+rewrite [in f _]addSn.
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 => idtac end.
+rewrite -[X in _ = X]addn0.
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0 => idtac end.
+rewrite -{2}[in X in _ = X](addn0 0).
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0) => idtac end.
+rewrite [_.+1 in X in f _ X](addnC x.+1).
+match goal with |- (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0) => idtac end.
+rewrite [x.+1 + y as X in f X _]addnC.
+match goal with |- (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) => idtac end.
+Admitted.
+
+Goal (exists x : 'I_3, x > 0).
+apply: (ex_intro _ (@Ordinal _ 2 _)).
+Admitted.
+
+Goal (forall y, 1 < y < 2 -> exists x : 'I_3, x > 0).
+move=> y; case/andP=> y_gt1 y_lt2; apply: (ex_intro _ (@Ordinal _ y _)).
+ by apply: leq_trans y_lt2 _.
+by move=> y_lt3; apply: leq_trans _ y_gt1.
+Qed.
+
+Goal (forall x y : nat, forall P : nat -> Prop, x = y -> True).
+move=> x y P E.
+have: P x -> P y by suff: x = y by move=> ?; congr (P _).
+Admitted.
+
+Goal forall a : bool, a -> true && a || false && a.
+by move=> a ?; rewrite [true && _]/= [_ && a]/= orbC [_ || _]//=.
+Qed.
+
+Goal forall a : bool, a -> true && a || false && a.
+by move=> a ?; rewrite [X in X || _]/= [X in _ || X]/= orbC [false && a as X in X || _]//=.
+Qed.
+
+Variable a : bool.
+Definition f x := x || a.
+Definition g x := f x.
+
+Goal a -> g false.
+by move=> Ha; rewrite [g _]/f orbC Ha.
+Qed.
+
+Goal a -> g false || g false.
+move=> Ha; rewrite {2}[g _]/f orbC Ha.
+match goal with |- (is_true (false || true || g false)) => done end.
+Qed.
+
+Goal a -> (a && a || true && a) && true.
+by move=> Ha; rewrite -[_ || _]/(g _) andbC /= Ha [g _]/f.
+Qed.
+
+Goal a -> (a || a) && true.
+by move=> Ha; rewrite -[in _ || _]/(f _) Ha andbC /f.
+Qed.
diff --git a/test-suite/ssr/set_lamda.v b/test-suite/ssr/set_lamda.v
new file mode 100644
index 000000000..a012ec680
--- /dev/null
+++ b/test-suite/ssr/set_lamda.v
@@ -0,0 +1,27 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool ssrfun.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+(* error 2 *)
+
+Goal (exists f: Set -> nat, f nat = 0).
+Proof. set (f:= fun _:Set =>0). by exists f. Qed.
+
+Goal (exists f: Set -> nat, f nat = 0).
+Proof. set f := (fun _:Set =>0). by exists f. Qed.
diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v
new file mode 100644
index 000000000..3ce75e879
--- /dev/null
+++ b/test-suite/ssr/set_pattern.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end.
+Ltac T2 x := first [set t := (x in RHS)].
+Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac].
+Ltac T4 x := set t := (x in RHS); idtac.
+Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end.
+
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Open Scope nat_scope.
+
+Lemma foo x y : x.+1 = y + x.+1.
+set t := (_.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in _ = x). match goal with |- x.+1 = t => rewrite /t {t} end.
+set t := (x in X in _ = X).
+ match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (x in RHS). match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t := (y + (1 + x) as X in _ = X).
+ match goal with |- x.+1 = t => rewrite /t addSn add0n {t} end.
+set t := x.+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := (x).+1. match goal with |- t = y + t => rewrite /t {t} end.
+set t := ((x).+1 in X in _ = X).
+ match goal with |- x.+1 = y + t => rewrite /t {t} end.
+set t := (x.+1 in RHS). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T1 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T2 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T3 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T4 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+T5 (x.+1). match goal with |- x.+1 = y + t => rewrite /t {t} end.
+rewrite [RHS]addnC.
+ match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end.
+rewrite -[in RHS](@subnK 1 x.+1) //.
+ match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end.
+have H : x.+1 = y by myadmit.
+set t := _.+1 in H |- *.
+ match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end.
+set t := (_.+1 in X in _ + X) in H |- *.
+ match goal with H : x.+1 = y |- x.+1 = y + t => rewrite /t {t} in H * end.
+set t := 0. match goal with t := 0 |- x.+1 = y + x.+1 => clear t end.
+set t := y + _. match goal with |- x.+1 = t => rewrite /t {t} end.
+set t : nat := 0. clear t.
+set t : nat := (x in RHS).
+ match goal with |- x.+1 = y + t.+1 => rewrite /t {t} end.
+set t : nat := RHS. match goal with |- x.+1 = t => rewrite /t {t} end.
+(* set t := 0 + _. *)
+(* set t := (x).+1 in X in _ + X in H |-. *)
+(* set t := (x).+1 in X in _ = X.*)
+Admitted.
diff --git a/test-suite/ssr/ssrsyntax2.v b/test-suite/ssr/ssrsyntax2.v
new file mode 100644
index 000000000..af839fabd
--- /dev/null
+++ b/test-suite/ssr/ssrsyntax2.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import TestSuite.ssr_ssrsyntax1.
+Require Import Arith.
+
+Goal (forall a b, a + b = b + a).
+intros.
+rewrite plus_comm, plus_comm.
+split.
+Qed.
diff --git a/test-suite/ssr/tc.v b/test-suite/ssr/tc.v
new file mode 100644
index 000000000..ae4589ef3
--- /dev/null
+++ b/test-suite/ssr/tc.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+
+Class foo (A : Type) : Type := mkFoo { val : A }.
+Instance foo_pair {A B} {f1 : foo A} {f2 : foo B} : foo (A * B) | 2 :=
+ {| val := (@val _ f1, @val _ f2) |}.
+Instance foo_nat : foo nat | 3 := {| val := 0 |}.
+
+Definition id {A} (x : A) := x.
+Axiom E : forall A {f : foo A} (a : A), id a = (@val _ f).
+
+Lemma test (x : nat) : id true = true -> id x = 0.
+Proof.
+Fail move=> _; reflexivity.
+Timeout 2 rewrite E => _; reflexivity.
+Qed.
+
+Definition P {A} (x : A) : Prop := x = x.
+Axiom V : forall A {f : foo A} (x:A), P x -> P (id x).
+
+Lemma test1 (x : nat) : P x -> P (id x).
+Proof.
+move=> px.
+Timeout 2 Fail move/V: px.
+Timeout 2 move/V : (px) => _.
+move/(V nat) : px => H; exact H.
+Qed.
diff --git a/test-suite/ssr/typeof.v b/test-suite/ssr/typeof.v
new file mode 100644
index 000000000..ca121fdb3
--- /dev/null
+++ b/test-suite/ssr/typeof.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+
+Ltac mycut x :=
+ let tx := type of x in
+ cut tx.
+
+Lemma test : True.
+Proof.
+by mycut I=> [ x | ]; [ exact x | exact I ].
+Qed.
diff --git a/test-suite/ssr/unfold_Opaque.v b/test-suite/ssr/unfold_Opaque.v
new file mode 100644
index 000000000..7c2b51de4
--- /dev/null
+++ b/test-suite/ssr/unfold_Opaque.v
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssreflect.
+
+Definition x := 3.
+Opaque x.
+
+Goal x = 3.
+Fail rewrite /x.
+Admitted.
diff --git a/test-suite/ssr/unkeyed.v b/test-suite/ssr/unkeyed.v
new file mode 100644
index 000000000..710941c30
--- /dev/null
+++ b/test-suite/ssr/unkeyed.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrfun ssrbool TestSuite.ssr_mini_mathcomp.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Import Prenex Implicits.
+
+Lemma test0 (a b : unit) f : a = f b.
+Proof. by rewrite !unitE. Qed.
+
+Lemma phE T : all_equal_to (Phant T). Proof. by case. Qed.
+
+Lemma test1 (a b : phant nat) f : a = f b.
+Proof. by rewrite !phE. Qed.
+
+Lemma eq_phE (T : eqType) : all_equal_to (Phant T). Proof. by case. Qed.
+
+Lemma test2 (a b : phant bool) f : a = locked (f b).
+Proof. by rewrite !eq_phE. Qed.
diff --git a/test-suite/ssr/view_case.v b/test-suite/ssr/view_case.v
new file mode 100644
index 000000000..2721470c4
--- /dev/null
+++ b/test-suite/ssr/view_case.v
@@ -0,0 +1,31 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+
+Axiom P : forall T, seq T -> Prop.
+
+Goal (forall T (s : seq T), P _ s).
+move=> T s.
+elim: s => [| x /lastP [| s] IH].
+Admitted.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> /ord1 -> /=; exact: refl_equal.
+Qed.
+
+Goal forall x : 'I_1, x = 0 :> nat.
+move=> x.
+move=> /ord1 -> in x |- *.
+exact: refl_equal.
+Qed.
diff --git a/test-suite/ssr/wlog_suff.v b/test-suite/ssr/wlog_suff.v
new file mode 100644
index 000000000..43a8f3b8b
--- /dev/null
+++ b/test-suite/ssr/wlog_suff.v
@@ -0,0 +1,28 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+
+Lemma test b : b || ~~b.
+wlog _ : b / b = true.
+ case: b; [ by apply | by rewrite orbC ].
+wlog suff: b / b || ~~b.
+ by case: b.
+by case: b.
+Qed.
+
+Lemma test2 b c (H : c = b) : b || ~~b.
+wlog _ : b {c H} / b = true.
+ by case: b H.
+by case: b.
+Qed.
diff --git a/test-suite/ssr/wlogletin.v b/test-suite/ssr/wlogletin.v
new file mode 100644
index 000000000..64e1ea84f
--- /dev/null
+++ b/test-suite/ssr/wlogletin.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Variable T : Type.
+Variables P : T -> Prop.
+
+Definition f := fun x y : T => x.
+
+Lemma test1 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+wlog H : @fxy Pfxy / P x.
+ match goal with |- (let fxy0 := f x y in P fxy0 -> P x -> P x) -> P x => by auto | _ => fail end.
+exact: H.
+Qed.
+
+Lemma test2 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+wlog H : fxy Pfxy / P x.
+ match goal with |- (forall fxy, P fxy -> P x -> P x) -> P x => by auto | _ => fail end.
+exact: H.
+Qed.
+
+Lemma test3 : forall x y : T, P (f x y) -> P x.
+Proof.
+move=> x y; set fxy := f x y; move=> Pfxy.
+move: {1}@fxy (Pfxy) (Pfxy).
+match goal with |- (let fxy0 := f x y in P fxy0 -> P fxy -> P x) => by auto | _ => fail end.
+Qed.
+
+Lemma test4 : forall n m z: bool, n = z -> let x := n in x = m && n -> x = m && n.
+move=> n m z E x H.
+case: true.
+ by rewrite {1 2}E in (x) H |- *.
+by rewrite {1}E in x H |- *.
+Qed.
diff --git a/test-suite/ssr/wlong_intro.v b/test-suite/ssr/wlong_intro.v
new file mode 100644
index 000000000..dd80f0435
--- /dev/null
+++ b/test-suite/ssr/wlong_intro.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
+
+Require Import ssreflect.
+Require Import ssrbool.
+Require Import TestSuite.ssr_mini_mathcomp.
+
+Goal (forall x y : nat, True).
+move=> x y.
+wlog suff: x y / x <= y.
+Admitted.
diff --git a/test-suite/unit-tests/.merlin b/test-suite/unit-tests/.merlin
new file mode 100644
index 000000000..b2279de74
--- /dev/null
+++ b/test-suite/unit-tests/.merlin
@@ -0,0 +1,6 @@
+REC
+
+S **
+B **
+
+PKG oUnit
diff --git a/test-suite/unit-tests/clib/inteq.ml b/test-suite/unit-tests/clib/inteq.ml
new file mode 100644
index 000000000..c07ec293f
--- /dev/null
+++ b/test-suite/unit-tests/clib/inteq.ml
@@ -0,0 +1,13 @@
+open Utest
+
+let eq0 = mk_bool_test "clib-inteq0"
+ "Int.equal on 0"
+ (Int.equal 0 0)
+
+let eq42 = mk_bool_test "clib-inteq42"
+ "Int.equal on 42"
+ (Int.equal 42 42)
+
+let tests = [ eq0; eq42 ]
+
+let _ = run_tests __FILE__ tests
diff --git a/test-suite/unit-tests/clib/unicode_tests.ml b/test-suite/unit-tests/clib/unicode_tests.ml
new file mode 100644
index 000000000..9ae405977
--- /dev/null
+++ b/test-suite/unit-tests/clib/unicode_tests.ml
@@ -0,0 +1,15 @@
+open Utest
+
+let unicode0 = mk_eq_test "clib-unicode0"
+ "split_at_first_letter, first letter is character"
+ None
+ (Unicode.split_at_first_letter "ident")
+
+let unicode1 = mk_eq_test "clib-unicode1"
+ "split_at_first_letter, first letter not character"
+ (Some ("__","ident"))
+ (Unicode.split_at_first_letter "__ident")
+
+let tests = [ unicode0; unicode1 ]
+
+let _ = run_tests __FILE__ tests
diff --git a/test-suite/unit-tests/src/utest.ml b/test-suite/unit-tests/src/utest.ml
new file mode 100644
index 000000000..069e6a4bf
--- /dev/null
+++ b/test-suite/unit-tests/src/utest.ml
@@ -0,0 +1,74 @@
+open OUnit
+
+(* general case to build a test *)
+let mk_test nm test = nm >: test
+
+(* common cases for building tests *)
+let mk_eq_test nm descr expected actual =
+ mk_test nm (TestCase (fun _ -> assert_equal ~msg:descr expected actual))
+
+let mk_bool_test nm descr actual =
+ mk_test nm (TestCase (fun _ -> assert_bool descr actual))
+
+let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "\n%!") oc)
+
+(* given test result, print message, return success boolean *)
+let logger out_ch result =
+ let cprintf s = cfprintf out_ch s in
+ match result with
+ | RSuccess path ->
+ cprintf "TEST SUCCEEDED: %s" (string_of_path path);
+ true
+ | RError (path,msg)
+ | RFailure (path,msg) ->
+ cprintf "TEST FAILED: %s (%s)" (string_of_path path) msg;
+ false
+ | RSkip (path,msg)
+ | RTodo (path,msg) ->
+ cprintf "TEST DID NOT SUCCEED: %s (%s)" (string_of_path path) msg;
+ false
+
+(* run one OUnit test case, return successes, no. of tests *)
+(* notionally one test, which might be a TestList *)
+let run_one logit test =
+ let rec process_results rs =
+ match rs with
+ [] -> (0,0)
+ | (r::rest) ->
+ let succ = if logit r then 1 else 0 in
+ let succ_results,tot_results = process_results rest in
+ (succ + succ_results,tot_results + 1)
+ in
+ let results = perform_test (fun _ -> ()) test in
+ process_results results
+
+(* run list of OUnit test cases, log results *)
+let run_tests ml_fn tests =
+ let log_fn = ml_fn ^ ".log" in
+ let out_ch = open_out log_fn in
+ let cprintf s = cfprintf out_ch s in
+ let ceprintf s = cfprintf stderr s in
+ let logit = logger out_ch in
+ let rec run_some tests succ tot =
+ match tests with
+ [] -> (succ,tot)
+ | (t::ts) ->
+ let succ_one,tot_one = run_one logit t in
+ run_some ts (succ + succ_one) (tot + tot_one)
+ in
+ (* format for test-suite summary to find status
+ success if all tests succeeded, else failure
+ *)
+ let succ,tot = run_some tests 0 0 in
+ cprintf
+ "*** Ran %d tests, with %d successes and %d failures ***"
+ tot succ (tot - succ);
+ if succ = tot then
+ cprintf
+ "==========> SUCCESS <==========\n %s...Ok" ml_fn
+ else begin
+ cprintf
+ "==========> FAILURE <==========\n %s...Error!" ml_fn;
+ ceprintf "FAILED %s.log" ml_fn
+ end;
+ close_out out_ch
diff --git a/test-suite/unit-tests/src/utest.mli b/test-suite/unit-tests/src/utest.mli
new file mode 100644
index 000000000..70928228b
--- /dev/null
+++ b/test-suite/unit-tests/src/utest.mli
@@ -0,0 +1,12 @@
+(** give a name to a unit test *)
+val mk_test : string -> OUnit.test -> OUnit.test
+
+(** simple ways to build a test *)
+val mk_eq_test : string -> string -> 'a -> 'a -> OUnit.test
+val mk_bool_test : string -> string -> bool -> OUnit.test
+
+(** run unit tests *)
+(* the string argument should be the name of the .ml file
+ containing the tests; use __FILE__ for that purpose.
+ *)
+val run_tests : string -> OUnit.test list -> unit