22 files changed, 130 insertions, 47 deletions
diff --git a/.gitignore b/.gitignore
index 582a8f43c7..0ab6e25852 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,7 +101,7 @@ doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
 doc/sphinx/zebibliography.rst
-doc/sphinx/credits-wrapper.rst
+doc/sphinx/credits.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 15fcdf371a..a6b17fd148 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -9,7 +9,7 @@ stages:
 variables:
   # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here
   # for reference]
-  CACHEKEY: "bionic_coq-V2018-09-23-V01"
+  CACHEKEY: "bionic_coq-V2018-09-24-V01"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
@@ -112,7 +112,7 @@ after_script:
     - not-a-real-job
   script:
     - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
-    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx
+    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= refman
     - make install-doc-sphinx
   artifacts:
     name: "$CI_JOB_NAME"
diff --git a/CHANGES b/CHANGES
index 45dba33a90..29b8fa1094 100644
--- a/CHANGES
+++ b/CHANGES
@@ -85,6 +85,11 @@ Specification language
   variables) may occasionally change type inference in incompatible
   ways, especially regarding the inference of the return clause of "match".
 
+- Fixing a missing check in interpreting instances of existential
+  variables which are bound to local definitions might exceptionally
+  induce an overhead if the cost of checking the conversion of the
+  corresponding definitions is additionally high (PR #8215).
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
@@ -95,6 +100,7 @@ Standard Library
   want).
 
 - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it.
+  Deprecated `Ndigits.N2Bv_gen`.
 
 - The scopes `int_scope` and `uint_scope` have been renamed to
   `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect
diff --git a/Makefile.doc b/Makefile.doc
index 788e4e61e7..db52607612 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -50,32 +50,35 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 ######################################################################
 
 .PHONY: doc doc-html doc-pdf doc-ps
-.PHONY: stdlib full-stdlib
+.PHONY: stdlib full-stdlib sphinx
 
-doc: sphinx stdlib
+doc: refman stdlib
 
 ifndef QUICK
 SPHINX_DEPS := coq
 endif
 
-# sphinx-html and sphinx-latex
-sphinx-%: $(SPHINX_DEPS)
+# refman-html and refman-latex
+refman-%: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx ($*)'
 	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \
 		$(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$*
 
-sphinx-pdf: sphinx-latex
+refman-pdf: refman-latex
 	+$(MAKE) -C $(SPHINXBUILDDIR)/latex
 
-sphinx: $(SPHINX_DEPS)
-	+$(MAKE) sphinx-html
-	+$(MAKE) sphinx-pdf
+refman: $(SPHINX_DEPS)
+	+$(MAKE) refman-html
+	+$(MAKE) refman-pdf
+
+# compatibility alias
+sphinx: refman-html
 
 doc-html:\
-  doc/stdlib/html/index.html sphinx-html
+  doc/stdlib/html/index.html refman-html
 
 doc-pdf:\
-  doc/stdlib/Library.pdf sphinx-pdf
+  doc/stdlib/Library.pdf refman-pdf
 
 doc-ps:\
   doc/stdlib/Library.ps
@@ -188,7 +191,7 @@ install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
-install-doc-html: install-doc-stdlib-html install-doc-sphinx-html
+install-doc-html: install-doc-stdlib-html install-doc-sphinx
 
 install-doc-stdlib-html:
 	$(MKDIR) $(FULLDOCDIR)/html/stdlib
@@ -199,7 +202,7 @@ install-doc-printable:
 	$(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
 	$(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps
 
-install-doc-sphinx-html:
+install-doc-sphinx:
 	$(MKDIR) $(FULLDOCDIR)/sphinx
 	(for f in `cd doc/sphinx/_build; find . -type f`; do \
 		$(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index b04161918e..8d0f69626e 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-09-23-V01"
+# CACHEKEY: "bionic_coq-V2018-09-24-V01"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.02.3"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \
-    CI_OPAM="menhir.20180530 elpi.1.0.5 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV CAMLP5_VER="6.14" \
diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh
new file mode 100644
index 0000000000..c08f44fc50
--- /dev/null
+++ b/dev/ci/user-overlays/08552-gares-elpi-11.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then
+    Elpi_CI_REF=coq-master-elpi-1.1
+fi
diff --git a/doc/README.md b/doc/README.md
index 1461fa2e2c..3db1261656 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -88,8 +88,11 @@ Alternatively, you can use some specific targets:
 - `make doc-html`
   to produce all HTML documents
 
-- `make sphinx`
-   to produce the HTML and PDF versions of the reference manual
+- `make refman`
+  to produce the HTML and PDF versions of the reference manual
+
+- `make refman-{html,pdf}`
+  to produce only one format of the reference manual
 
 - `make stdlib`
   to produce all formats of the Coq standard library
@@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors.  Otherwise, Sphinx quits
 upon detecting the first warning.  You can set this on the Sphinx `make`
 command line or as an environment variable:
 
-- `make sphinx SPHINXWARNERROR=0`
+- `make refman SPHINXWARNERROR=0`
 
 - ~~~
   export SPHINXWARNERROR=0
     ⋮
-  make sphinx
+  make refman
   ~~~
 
 Installation
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 904945a58d..4ad952bdfb 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -292,7 +292,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
           \WTEG{\forall~x:T,U}{\Prop}
 
 ``.. preamble::`` A reST directive to include a TeX file.
-    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.  The
+    contents of the TeX file are wrapped in a math environment, as MathJax
+    doesn't process LaTeX definitions otherwise.
 
     Usage::
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index b43d5fb6f0..71f01cbb17 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -106,7 +106,7 @@ def setup(app):
 master_doc = "index"
 
 # General information about the project.
-project = 'The Coq Reference Manual'
+project = 'Coq'
 copyright = '1999-2018, Inria'
 author = 'The Coq Development Team'
 
@@ -335,7 +335,7 @@ latex_additional_files = [
     "_static/coqnotations.sty"
 ]
 
-latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
+latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')]
 
 # The name of an image file (relative to this directory) to place at the top of
 # the title page.
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst
index 212f0a65b0..212f0a65b0 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits-contents.rst
diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst
deleted file mode 100644
index 9f7dd49af8..0000000000
--- a/doc/sphinx/credits-wrapper.latex.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-.. _credits:
-
-.. include:: credits.rst
diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst
index 2d35a12dc2..0b2b1c6ad1 100644
--- a/doc/sphinx/credits-wrapper.html.rst
+++ b/doc/sphinx/credits.html.rst
@@ -4,4 +4,4 @@
 Credits
 -------
 
-.. include:: credits.rst
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst
new file mode 100644
index 0000000000..39101f9d52
--- /dev/null
+++ b/doc/sphinx/credits.latex.rst
@@ -0,0 +1,3 @@
+.. _credits:
+
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 9d90857061..cf12b57414 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,11 +1,8 @@
-==========================
- The Coq Reference Manual
-==========================
-
 .. _introduction:
 
+==========================
 Introduction
-------------
+==========================
 
 .. include:: introduction.rst
 
@@ -28,7 +25,7 @@ Table of contents
    :caption: Preamble
 
    self
-   credits-wrapper
+   credits
 
 .. toctree::
    :caption: The language
@@ -89,3 +86,8 @@ License
 -------
 
 .. include:: license.rst
+
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+   Optionally, you can enhance it with the minor mode
+   Company-Coq :cite:`Pit16`
+   (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 0f2f7b4897..af757f8746 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -7,10 +7,15 @@ Introduction
 
 .. include:: introduction.rst
 
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+   Optionally, you can enhance it with the minor mode
+   Company-Coq :cite:`Pit16`
+   (see https://github.com/cpitclaudel/company-coq).
+
 Credits
 -------
 
-.. include:: credits-wrapper.rst
+.. include:: credits.rst
 
 License
 -------
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b8d2f6b6dc..5bb7bf542c 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -35,11 +35,6 @@ are processed from a file.
    The `coqtop` read-eval-print-loop can also be used directly, for debugging
    purposes.
 
-   .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
-      Optionally, you can enhance it with the minor mode
-      Company-Coq :cite:`Pit16`
-      (see https://github.com/cpitclaudel/company-coq).
-
 -  The compiled mode acts as a proof checker taking a file containing a
    whole development in order to ensure its correctness. Moreover,
    |Coq|’s compiler provides an output file containing a compact
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 97dabbf815..edf4e6ec9d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -666,7 +666,9 @@ class ExampleDirective(BaseAdmonition):
 class PreambleDirective(Directive):
     r"""A reST directive to include a TeX file.
 
-    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
+    Mostly useful to let MathJax know about `\def`s and `\newcommand`s.  The
+    contents of the TeX file are wrapped in a math environment, as MathJax
+    doesn't process LaTeX definitions otherwise.
 
     Usage::
 
@@ -693,7 +695,7 @@ class PreambleDirective(Directive):
         with open(abs_fname, encoding="utf-8") as ltx:
             latex = ltx.read()
 
-        node = make_math_node(latex, env.docname, nowrap=True)
+        node = make_math_node(latex, env.docname, nowrap=False)
         node['classes'] = ["math-preamble"]
         set_source_info(self, node)
         return [node]
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d10c00fa6e..e3aa90fbcf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -960,20 +960,50 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
   let f decl (subst,update) =
     let id = NamedDecl.get_id decl in
+    let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
     let t = replace_vars subst (NamedDecl.get_type decl) in
+    let check_body id c =
+      match b, c with
+      | Some b, Some c ->
+         if not (is_conv !!env !evdref b c) then
+           user_err ?loc  (str "Cannot interpret " ++
+             pr_existential_key !evdref evk ++
+             strbrk " in current context: binding for " ++ Id.print id ++
+             strbrk " is not convertible to its expected definition (cannot unify " ++
+             quote (print_constr_env !!env !evdref b) ++
+             strbrk " and " ++
+             quote (print_constr_env !!env !evdref c) ++
+             str ").")
+      | Some b, None ->
+           user_err ?loc  (str "Cannot interpret " ++
+             pr_existential_key !evdref evk ++
+             strbrk " in current context: " ++ Id.print id ++
+             strbrk " should be bound to a local definition.")
+      | None, _ -> () in
+    let check_type id t' =
+      if not (is_conv !!env !evdref t t') then
+        user_err ?loc  (str "Cannot interpret " ++
+          pr_existential_key !evdref evk ++
+          strbrk " in current context: binding for " ++ Id.print id ++
+          strbrk " is not well-typed.") in
     let c, update =
       try
         let c = List.assoc id update in
         let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in
+        check_body id (Some c.uj_val);
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
-        let (n,_,t') = lookup_rel_id id (rel_context !!env) in
-        if is_conv !!env !evdref t (lift n t') then mkRel n, update else raise Not_found
+        let (n,b',t') = lookup_rel_id id (rel_context !!env) in
+        check_type id (lift n t');
+        check_body id (Option.map (lift n) b');
+        mkRel n, update
       with Not_found ->
       try
-        let t' = !!env |> lookup_named id |> NamedDecl.get_type in
-        if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found
+        let decl = lookup_named id !!env in
+        check_type id (NamedDecl.get_type decl);
+        check_body id (NamedDecl.get_value decl);
+        mkVar id, update
       with Not_found ->
         user_err ?loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v
new file mode 100644
index 0000000000..c4b29a6354
--- /dev/null
+++ b/test-suite/bugs/closed/8215.v
@@ -0,0 +1,14 @@
+(* Check that instances for local definitions in evars have compatible body *)
+Goal False.
+Proof.
+  pose (n := 1).
+  evar (m:nat).
+  subst n.
+  pose (n := 0).
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clearbody n.
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clear n.
+  pose (n := 0+1).
+  Check ?m. (* Should be ok *)
+Abort.
diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v
new file mode 100644
index 0000000000..00aa66e701
--- /dev/null
+++ b/test-suite/bugs/closed/8532.v
@@ -0,0 +1,8 @@
+(* Checking Print Assumptions relatively to a bound module *)
+
+Module Type Typ.
+  Parameter Inline(10) t : Type.
+End Typ.
+Module  Terms_mod (SetVars : Typ).
+Print Assumptions SetVars.t.
+End Terms_mod.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 68a98e4292..a2a2430e91 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -578,6 +578,7 @@ Qed.
 (** To state nonetheless a second result about composition of
  conversions, we define a conversion on a given number of bits : *)
 
+#[deprecated(since = "8.9.0", note = "Use N2Bv_sized instead.")]
 Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
  match n return Bvector n with
    | 0 => Bnil
@@ -705,3 +706,10 @@ Proof with simpl; auto.
   destruct (Bv2N n v) as [|[]];
   rewrite <- IHv...
 Qed.
+
+Lemma N2Bv_N2Bv_sized_above (a : N) (k : nat) :
+  N2Bv_sized (N.size_nat a + k) a = N2Bv a ++ Bvect_false k.
+Proof with auto.
+  destruct a...
+  induction p; simpl; f_equal...
+Qed.
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 0bcd3c64eb..b000745961 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -71,7 +71,7 @@ let rec fields_of_functor f subs mp0 args = function
 let rec lookup_module_in_impl mp =
     match mp with
     | MPfile _ -> Global.lookup_module mp
-    | MPbound _ -> assert false
+    | MPbound _ -> Global.lookup_module mp
     | MPdot (mp',lab') ->
        if ModPath.equal mp' (Global.current_modpath ()) then
          Global.lookup_module mp