18 files changed, 356 insertions, 310 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d45c4647d..0bc67dfcc 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -50,11 +50,13 @@ before_script:
 # TODO figure out how to build doc for installed Coq
 .build-template: &build-template
   stage: build
+  retry: 1
   artifacts:
     name: "$CI_JOB_NAME"
     paths:
       - _install_ci
       - config/Makefile
+      - config/coq_config.py
       - test-suite/misc/universes/all_stdlib.v
     expire_in: 1 week
   script:
@@ -70,7 +72,7 @@ before_script:
 
     - echo 'start:coq.build'
     - make -j "$NJOBS" byte
-    - make -j "$NJOBS"
+    - make -j "$NJOBS" world $EXTRA_TARGET
     - make test-suite/misc/universes/all_stdlib.v
     - echo 'end:coq:build'
 
@@ -109,6 +111,19 @@ before_script:
 # purpose, we add a spurious dependency `not-a-real-job` that must be
 # overridden otherwise the CI will fail.
 
+.doc-templare: &doc-template
+  stage: test
+  dependencies:
+    - not-a-real-job
+  script:
+    - SPHINXENV='COQBIN="'"$PWD"'/_install_ci/bin/" COQBOOT=no'
+    - make -j "$NJOBS" SPHINXENV="$SPHINXENV" SPHINX_DEPS= sphinx
+    - make install-doc-sphinx
+  artifacts:
+    name: "$CI_JOB_NAME"
+    paths:
+      - _install_ci/share/doc/coq/
+
 # set dependencies when using
 .test-suite-template: &test-suite-template
   stage: test
@@ -181,7 +196,9 @@ before_script:
 build:base:
   <<: *build-template
   variables:
-    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -with-doc yes"
+    COQ_EXTRA_CONF: "-native-compiler yes -coqide opt"
+    # coqdoc for stdlib, until we know how to build it from installed Coq
+    EXTRA_TARGET: "stdlib"
 
 # no coqide for 32bit: libgtk installation problems
 build:base+32bit:
@@ -228,6 +245,11 @@ warnings:edge:
     <<: *warnings-variables
     OPAM_SWITCH: edge
 
+documentation:
+  <<: *doc-template
+  dependencies:
+    - build:base
+
 test-suite:base:
   <<: *test-suite-template
   dependencies:
diff --git a/Makefile.doc b/Makefile.doc
index 4670c79ec..dde3a37b7 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -31,6 +31,7 @@ DVIPS:=dvips
 HTMLSTYLE:=coqremote
 
 # Sphinx-related variables
+SPHINXENV:=COQBIN="$(CURDIR)/bin/"
 SPHINXOPTS= -j4
 SPHINXBUILD= sphinx-build
 SPHINXBUILDDIR= doc/sphinx/_build
@@ -55,7 +56,7 @@ endif
 
 sphinx: $(SPHINX_DEPS)
 	$(SHOW)'SPHINXBUILD doc/sphinx'
-	$(HIDE)COQBIN="$(abspath bin)" $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
+	$(HIDE)$(SPHINXENV) $(SPHINXBUILD) -W -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html
 	@echo
 	@echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html."
 
diff --git a/clib/cList.ml b/clib/cList.ml
index 646e39d23..2b627f745 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -116,6 +116,7 @@ sig
   val subtract : 'a eq -> 'a list -> 'a list -> 'a list
   val subtractq : 'a list -> 'a list -> 'a list
   val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+  [@@ocaml.deprecated "Same as [merge_set]"]
   val distinct : 'a list -> bool
   val distinct_f : 'a cmp -> 'a list -> bool
   val duplicates : 'a eq -> 'a list -> 'a list
diff --git a/clib/cList.mli b/clib/cList.mli
index d080ebca2..13e069e94 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -354,7 +354,7 @@ sig
   (** [subtract] specialized to physical equality *)
 
   val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list
-  (** [@@ocaml.deprecated "Same as [merge_set]"] *)
+  [@@ocaml.deprecated "Same as [merge_set]"]
 
   (** {6 Uniqueness and duplication} *)
 
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 5b5cbd11a..85df249d3 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -93,17 +93,26 @@ install_ssreflect()
   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 && \
-    sed -i.bak '/all\/all.v/d'  Make && \
-    sed -i.bak '/character/d'   Make && \
-    sed -i.bak '/real_closed/d' Make && \
-    sed -i.bak '/solvable/d'    Make && \
-    sed -i.bak '/field/d'       Make && \
-    sed -i.bak '/fingroup/d'    Make && \
-    sed -i.bak '/algebra/d'     Make && \
-    make Makefile.coq && make -f Makefile.coq all && make install )
+    make Makefile.coq && \
+    make -f Makefile.coq ssreflect/all_ssreflect.vo && \
+    make -f Makefile.coq install )
 
   echo -en 'travis_fold:end:ssr.install\\r'
 
 }
+
+# this installs just the ssreflect + algebra library of math-comp
+install_ssralg()
+{
+  echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r'
+
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
+  ( cd "${mathcomp_CI_DIR}/mathcomp" && \
+    make Makefile.coq && \
+    make -f Makefile.coq algebra/all_algebra.vo && \
+    make -f Makefile.coq install )
+
+  echo -en 'travis_fold:end:ssralg.install\\r'
+
+}
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 920272bcf..24cd9c427 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -7,4 +7,6 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
 git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
+install_ssralg
+
 ( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make )
diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md
new file mode 100644
index 000000000..ea76aeeab
--- /dev/null
+++ b/dev/doc/primproj.md
@@ -0,0 +1,41 @@
+Primitive Projections
+---------------------
+
+    | Proj of Projection.t * constr
+
+Projections are always applied to a term, which must be of a record
+type (i.e. reducible to an inductive type `I params`). Type-checking,
+reduction and conversion are fast (not as fast as they could be yet)
+because we don't keep parameters around. As you can see, it's
+currently a `constant` that is used here to refer to the projection,
+that will change to an abstract `projection` type in the future.
+Basically a projection constant records which inductive it is a
+projection for, the number of params and the actual position in the
+constructor that must be projected. For compatibility reason, we also
+define an eta-expanded form (accessible from user syntax `@f`). The
+constant_entry of a projection has both informations. Declaring a
+record (under `Set Primitive Projections`) will generate such
+definitions. The API to declare them is not stable at the moment, but
+the inductive type declaration also knows about the projections, i.e.
+a record inductive type decl contains an array of terms representing
+the projections. This is used to implement eta-conversion for record
+types (with at least one field and having all projections definable).
+The canonical value being `Build_R (pn x) ... (pn x)`. Unification and
+conversion work up to this eta rule. The records can also be universe
+polymorphic of course, and we don't need to keep track of the universe
+instance for the projections either. Projections are reduced _eagerly_
+everywhere, and introduce a new `Zproj` constructor in the abstract
+machines that obeys both the delta (for the constant opacity) and iota
+laws (for the actual reduction). Refolding works as well (afaict), but
+there is a slight hack there related to universes (not projections).
+
+For the ML programmer, the biggest change is that pattern-matchings on
+kind_of_term require an additional case, that is handled usually
+exactly like an `App (Const p) arg`.
+
+There are slight hacks related to hints is well, to use the primitive
+projection form of f when one does `Hint Resolve f`. Usually hint
+resolve will typecheck the term, resulting in a partially applied
+projection (disallowed), so we allow it to take
+`constr_or_global_reference` arguments instead and special-case on
+projections. Other tactic extensions might need similar treatment.
diff --git a/dev/doc/univpoly.txt b/dev/doc/universes.md
index ca3d520c7..c276603ed 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/universes.md
@@ -1,11 +1,11 @@
-Notes on universe polymorphism and primitive projections, M. Sozeau
-===================================================================
+Notes on universe polymorphism
+------------------------------
 
-The new implementation of universe polymorphism and primitive
-projections introduces a few changes to the API of Coq. First and
-foremost, the term language changes, as global references now carry a
-universe level substitution:
+The implementation of universe polymorphism introduces a few changes
+to the API of Coq. First and foremost, the term language changes, as
+global references now carry a universe level substitution:
 
+~~~ocaml
 type 'a puniverses = 'a * Univ.Instance.t
 type pconstant = constant puniverses
 type pinductive = inductive puniverses
@@ -15,30 +15,31 @@ type constr = ...
   | Const of puniverses
   | Ind of pinductive
   | Constr of pconstructor
-  | Proj of constant * constr
-
+~~~
 
 Universes
-=========
+---------
 
-  Universe instances (an array of levels) gets substituted when
+Universe instances (an array of levels) gets substituted when
 unfolding definitions, are used to typecheck and are unified according
-to the rules in the ITP'14 paper on universe polymorphism in Coq.  
+to the rules in the ITP'14 paper on universe polymorphism in Coq.
 
+~~~ocaml
 type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *)
 type Instance.t = Level.t array
 type Universe.t = Level.t list (* hashconsed *)
+~~~
 
 The universe module defines modules and abstract types for levels,
 universes etc.. Structures are hashconsed (with a hack to take care
-of the fact that deserialization breaks sharing). 
+of the fact that deserialization breaks sharing).
 
-  Definitions (constants, inductives) now carry around not only 
+  Definitions (constants, inductives) now carry around not only
 constraints but also the universes they introduced (a Univ.UContext.t).
-There is another kind of contexts [Univ.ContextSet.t], the latter has 
+There is another kind of contexts `Univ.ContextSet.t`, the latter has
 a set of universes, while the former has serialized the levels in an
-array, and is used for polymorphic objects. Both have "reified" 
-constraints depending on global and local universes. 
+array, and is used for polymorphic objects. Both have "reified"
+constraints depending on global and local universes.
 
   A polymorphic definition is abstract w.r.t. the variables in this
 context, while a monomorphic one (or template polymorphic) just adds the
@@ -46,18 +47,18 @@ universes and constraints to the global universe context when it is put
 in the environment. No other universes than the global ones and the
 declared local ones are needed to check a declaration, hence the kernel
 does not produce any constraints anymore, apart from module
-subtyping.... There are hence two conversion functions now: [check_conv]
-and [infer_conv]: the former just checks the definition in the current env
+subtyping.... There are hence two conversion functions now: `check_conv`
+and `infer_conv`: the former just checks the definition in the current env
 (in which we usually push_universe_context of the associated context),
-and [infer_conv] which produces constraints that were not implied by the
+and `infer_conv` which produces constraints that were not implied by the
 ambient constraints. Ideally, that one could be put out of the kernel,
-but currently module subtyping needs it. 
+but currently module subtyping needs it.
 
  Inference of universes is now done during refinement, and the evar_map
 carries the incrementally built universe context, starting from the
-global universe constraints (see [Evd.from_env]). [Evd.conversion] is a
-wrapper around [infer_conv] that will do the bookkeeping for you, it
-uses [evar_conv_x]. There is a universe substitution being built
+global universe constraints (see `Evd.from_env`). `Evd.conversion` is a
+wrapper around `infer_conv` that will do the bookkeeping for you, it
+uses `evar_conv_x`. There is a universe substitution being built
 incrementally according to the constraints, so one should normalize at
 the end of a proof (or during a proof) with that substitution just like
 we normalize evars. There are some nf_* functions in
@@ -67,16 +68,16 @@ the universe constraints used in the term. It is heuristic but
 validity-preserving. No user-introduced universe (i.e. coming from a
 user-written anonymous Type) gets touched by this, only the fresh
 universes generated for each global application. Using
-
+~~~ocaml
 val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic
-
+~~~
 Is the way to make a constr out of a global reference in the new API.
 If they constr is polymorphic, it will add the necessary constraints to
 the evar_map. Even if a constr is not polymorphic, we have to take care
 of keeping track of its universes. Typically, using:
-
-  mkApp (coq_id_function, [| A; a |]) 
-
+~~~ocaml
+  mkApp (coq_id_function, [| A; a |])
+~~~
 and putting it in a proof term is not enough now. One has to somehow
 show that A's type is in cumululativity relation with id's type
 argument, incurring a universe constraint. To do this, one can simply
@@ -84,19 +85,19 @@ call Typing.resolve_evars env evdref c which will do some infer_conv to
 produce the right constraints and put them in the evar_map. Of course in
 some cases you might know from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
-forgot some. As a temporary way out, [Universes.constr_of_global] allows
+forgot some. As a temporary way out, `Universes.constr_of_global` allows
 you to make a constr from any non-polymorphic constant, but it will fail
 on polymorphic ones.
 
 Other than that, unification (w_unify and evarconv) now take account of universes and
 produce only well-typed evar_maps.
 
-Some syntactic comparisons like the one used in [change] have to be
-adapted to allow identification up-to-universes (when dealing with 
-polymorphic references), [make_eq_univs_test] is there to help. 
+Some syntactic comparisons like the one used in `change` have to be
+adapted to allow identification up-to-universes (when dealing with
+polymorphic references), `make_eq_univs_test` is there to help.
 In constr, there are actually many new comparison functions to deal with
 that:
- 
+~~~ocaml
 (** [equal a b] is true if [a] equals [b] modulo alpha, casts,
    and application grouping *)
 val equal : constr -> constr -> bool
@@ -105,7 +106,7 @@ val equal : constr -> constr -> bool
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
 
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
     alpha, casts, application grouping and the universe inequalities in [u]. *)
 val leq_constr_univs : constr Univ.check_function
 
@@ -120,47 +121,47 @@ val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
-
-The [_univs] versions are doing checking of universe constraints
-according to a graph, while the [_universes] are producing (non-atomic) 
+~~~
+The `_univs` versions are doing checking of universe constraints
+according to a graph, while the `_universes` are producing (non-atomic)
 universe constraints. The non-atomic universe constraints include the
-[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2'
-*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are
-treated specially: as unfolding [f] might not result in these
+`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2'
+*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are
+treated specially: as unfolding `f` might not result in these
 unifications, we need to keep track of the fact that failure to satisfy
 them does not mean that the term are actually equal. This is used in
-unification but probably not necessary to the average programmer. 
+unification but probably not necessary to the average programmer.
 
 Another issue for ML programmers is that tables of constrs now usually
-need to take a [constr Univ.in_universe_context_set] instead, and
-properly refresh the universes context when using the constr, e.g. using 
-Clenv.refresh_undefined_univs clenv or: 
-
+need to take a `constr Univ.in_universe_context_set` instead, and
+properly refresh the universes context when using the constr, e.g. using
+Clenv.refresh_undefined_univs clenv or:
+~~~ocaml
 (** Get fresh variables for the universe context.
     Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
-val fresh_universe_context_set_instance : universe_context_set -> 
+val fresh_universe_context_set_instance : universe_context_set ->
   universe_level_subst * universe_context_set
-
-The substitution should be applied to the constr(s) under consideration, 
+~~~
+The substitution should be applied to the constr(s) under consideration,
 and the context_set merged with the current evar_map with:
-
+~~~ocaml
 val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map
-
-The [rigid] flag here should be [Evd.univ_flexible] most of the
+~~~
+The `rigid` flag here should be `Evd.univ_flexible` most of the
 time. This means the universe levels of polymorphic objects in the
-constr might get instantiated instead of generating equality constraints 
+constr might get instantiated instead of generating equality constraints
 (Evd.univ_rigid does that).
 
-On this issue, I recommend forcing commands to take [global_reference]s
+On this issue, I recommend forcing commands to take `global_reference`s
 only, the user can declare his specialized terms used as hints as
 constants and this is cleaner. Alas, backward-compatibility-wise,
 this is the only solution I found. In the case of global_references
-only, it's just a matter of using [Evd.fresh_global] /
-[pf_constr_of_global] to let the system take care of universes.
+only, it's just a matter of using `Evd.fresh_global` /
+`pf_constr_of_global` to let the system take care of universes.
 
 
 The universe graph
-==================
+------------------
 
 To accomodate universe polymorphic definitions, the graph structure in
 kernel/univ.ml was modified. The new API forces every universe to be
@@ -176,68 +177,14 @@ no universe i can be set lower than Set, so the chain of universes
 always bottoms down at Prop < Set.
 
 Modules
-=======
+-------
 
 One has to think of universes in modules as being globally declared, so
 when including a module (type) which declares a type i (e.g. through a
 parameter), we get back a copy of i and not some fresh universe.
 
-Projections
-===========
-
-  | Proj of constant * constr
-
-Projections are always applied to a term, which must be of a record type
-(i.e. reducible to an inductive type [I params]). Type-checking,
-reduction and conversion are fast (not as fast as they could be yet)
-because we don't keep parameters around. As you can see, it's currently
-a [constant] that is used here to refer to the projection, that will
-change to an abstract [projection] type in the future. Basically a
-projection constant records which inductive it is a projection for, the
-number of params and the actual position in the constructor that must be
-projected. For compatibility reason, we also define an eta-expanded form
-(accessible from user syntax @f). The constant_entry of a projection has
-both informations. Declaring a record (under [Set Primitive
-Projections]) will generate such definitions. The API to declare them is
-not stable at the moment, but the inductive type declaration also knows
-about the projections, i.e. a record inductive type decl contains an
-array of terms representing the projections. This is used to implement
-eta-conversion for record types (with at least one field and having all
-projections definable). The canonical value being [Build_R (pn x)
-... (pn x)]. Unification and conversion work up to this eta rule. The
-records can also be universe polymorphic of course, and we don't need to
-keep track of the universe instance for the projections either.
-Projections are reduced _eagerly_ everywhere, and introduce a new Zproj
-constructor in the abstract machines that obeys both the delta (for the
-constant opacity) and iota laws (for the actual reduction). Refolding
-works as well (afaict), but there is a slight hack there related to
-universes (not projections). 
-
-For the ML programmer, the biggest change is that pattern-matchings on
-kind_of_term require an additional case, that is handled usually exactly
-like an [App (Const p) arg].
-
-There are slight hacks related to hints is well, to use the primitive
-projection form of f when one does [Hint Resolve f]. Usually hint
-resolve will typecheck the term, resulting in a partially applied
-projection (disallowed), so we allow it to take
-[constr_or_global_reference] arguments instead and special-case on
-projections. Other tactic extensions might need similar treatment. 
-
-WIP
-===
-
-- [vm_compute] does not deal with universes and projections correctly,
-except when it goes to a normal form with no projections or polymorphic
-constants left (the most common case). E.g. Ring with Set Universe
-Polymorphism and Set Primitive Projections work (at least it did at some
-point, I didn't recheck yet).  
-
-- [native_compute] works with universes and projections.
-
-
 Incompatibilities
-=================
+-----------------
 
 Old-style universe polymorphic definitions were implemented by taking
 advantage of the fact that elaboration (i.e., pretyping and unification)
@@ -247,33 +194,33 @@ possible, as unification ensures that the substitution is built is
 entirely well-typed, even w.r.t universes. This means that some terms
 that type-checked before no longer do, especially projections of the
 pair:
-
+~~~coq
 @fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)).
-
+~~~
 The "template universe polymorphic" variables i and j appear during
 typing without being refreshed, meaning that they can be lowered (have
 upper constraints) with user-introduced universes. In most cases this
 won't work, so ?x and ?y have to be instantiated earlier, either from
 the type of the actual projected pair term (some t : prod A B) or the
-typing constraint. Adding the correct type annotations will always fix 
+typing constraint. Adding the correct type annotations will always fix
 this.
 
 
 Unification semantics
-=====================
+---------------------
 
 In Ltac, matching with:
 
-- a universe polymorphic constant [c] matches any instance of the
+- a universe polymorphic constant `c` matches any instance of the
   constant.
-- a variable ?x already bound to a term [t] (non-linear pattern) uses 
+- a variable ?x already bound to a term `t` (non-linear pattern) uses
   strict equality of universes (e.g., Type@{i} and Type@{j} are not
   equal).
 
 In tactics:
 
-- [change foo with bar], [pattern foo] will unify all instances of [foo]
-  (and convert them with [bar]). This might incur unifications of
-  universes. [change] uses conversion while [pattern] only does
+- `change foo with bar`, `pattern foo` will unify all instances of `foo`
+  (and convert them with `bar`). This might incur unifications of
+  universes. `change` uses conversion while `pattern` only does
   syntactic matching up-to unification of universes.
-- [apply], [refine] use unification up to universes.
+- `apply`, `refine` use unification up to universes.
diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt
deleted file mode 100644
index a40706e99..000000000
--- a/dev/doc/universes.txt
+++ /dev/null
@@ -1,26 +0,0 @@
-How to debug universes?
-
-1. There is a command Print Universes in Coq toplevel
-
-   Print Universes.
-     prints the graph of universes in the form of constraints
-
-   Print Universes "file".
-     produces the "file" containing universe constraints in the form
-       univ1 # univ2 ;
-     where # can be either > >= or =
-
-   If "file" ends with .gv or .dot, the resulting file will be in
-   dot format.
-
-
-   *) for dot see http://www.research.att.com/sw/tools/graphviz/
-
-
-2. There is a printing option
-
-   {Set,Unset} Printing Universes.
-
-   which, when set, makes all pretty-printed Type's annotated with the
-   name of the universe.
-
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 63cd0f3ea..3b2009657 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -37,7 +37,7 @@ bookkeeping is performed on the conclusion of the goal, using for that
 purpose a couple of syntactic constructions behaving similar to tacticals
 (and often named as such in this chapter). The ``:`` tactical moves hypotheses
 from the context to the conclusion, while ``=>`` moves hypotheses from the
-conclusion to the context, and in moves back and forth an hypothesis from the
+conclusion to the context, and ``in`` moves back and forth an hypothesis from the
 context to the conclusion for the time of applying an action to it.
 
 While naming hypotheses is commonly done by means of an ``as`` clause in the
@@ -47,20 +47,22 @@ often followed by ``=>`` to explicitly name them. While generalizing the
 goal is normally not explicitly needed in Chapter :ref:`tactics`, it is an
 explicit operation performed by ``:``.
 
+.. seealso:: :ref:`bookkeeping_ssr`
+
 Beside the difference of bookkeeping model, this chapter includes
 specific tactics which have no explicit counterpart in Chapter :ref:`tactics`
-such as tactics to mix forward steps and generalizations as generally
-have or without loss.
+such as tactics to mix forward steps and generalizations as
+:tacn:`generally have` or :tacn:`without loss`.
 
 |SSR| adopts the point of view that rewriting, definition
 expansion and partial evaluation participate all to a same concept of
 rewriting a goal in a larger sense. As such, all these functionalities
-are provided by the rewrite tactic.
+are provided by the :tacn:`rewrite <rewrite (ssreflect)>` tactic.
 
 |SSR| includes a little language of patterns to select subterms in
 tactics or tacticals where it matters. Its most notable application is
-in the rewrite tactic, where patterns are used to specify where the
-rewriting step has to take place.
+in the :tacn:`rewrite <rewrite (ssreflect)>` tactic, where patterns are
+used to specify where the rewriting step has to take place.
 
 Finally, |SSR| supports so-called reflection steps, typically
 allowing to switch back and forth between the computational view and
@@ -87,20 +89,24 @@ Getting started
 ~~~~~~~~~~~~~~~
 
 To be available, the tactics presented in this manual need the
-following minimal set of libraries to loaded: ``ssreflect.v``,
+following minimal set of libraries to be loaded: ``ssreflect.v``,
 ``ssrfun.v`` and ``ssrbool.v``.
 Moreover, these tactics come with a methodology
 specific to the authors of |SSR| and which requires a few options
 to be set in a different way than in their default way. All in all,
 this corresponds to working in the following context:
 
-.. coqtop:: all
+.. coqtop:: in
 
    From Coq Require Import ssreflect ssrfun ssrbool.
    Set Implicit Arguments.
    Unset Strict Implicit.
    Unset Printing Implicit Defensive.
 
+.. seealso::
+   :opt:`Implicit Arguments`, :opt:`Strict Implicit`,
+   :opt:`Printing Implicit Defensive`
+
 .. _compatibility_issues_ssr:
 
 
@@ -114,14 +120,14 @@ compatible with the rest of |Coq|, up to a few discrepancies:
 + New keywords (``is``) might clash with variable, constant, tactic or
   tactical names, or with quasi-keywords in tactic or vernacular
   notations.
-+ New tactic(al)s names (``last``, ``done``, ``have``, ``suffices``,
-  ``suff``, ``without loss``, ``wlog``, ``congr``, ``unlock``)
++ New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`,
+  :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`)
   might clash with user tactic names.
 + Identifiers with both leading and trailing ``_``, such as ``_x_``, are
   reserved by |SSR| and cannot appear in scripts.
-+ The extensions to the rewrite tactic are partly incompatible with those
++ The extensions to the :tacn:`rewrite` tactic are partly incompatible with those
   available in current versions of |Coq|; in particular: ``rewrite .. in
-  (type of k)`` or ``rewrite .. in *`` or any other variant of ``rewrite``
+  (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite`
   will not work, and the |SSR| syntax and semantics for occurrence selection
   and rule chaining is different. Use an explicit rewrite direction
   (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic.
@@ -139,7 +145,7 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   Note that the full
   syntax of |SSR|’s rewrite and reserved identifiers are enabled
   only if the ssreflect module has been required and if ``SsrSyntax`` has
-  been imported. Thus a file that requires (without importing) ssreflect
+  been imported. Thus a file that requires (without importing) ``ssreflect``
   and imports ``SsrSyntax``, can be required and imported without
   automatically enabling |SSR|’s extended rewrite syntax and
   reserved identifiers.
@@ -148,9 +154,10 @@ compatible with the rest of |Coq|, up to a few discrepancies:
   such as have, set and pose.
 + The generalization of if statements to non-Boolean conditions is turned off
   by |SSR|, because it is mostly subsumed by Coercion to ``bool`` of the
-  ``sumXXX`` types (declared in ``ssrfun.v``) and the ``if`` *term* ``is`` *pattern* ``then``
-  *term* ``else`` *term* construct (see :ref:`pattern_conditional_ssr`).  To use the
-  generalized form, turn off the |SSR| Boolean if notation using the command:
+  ``sumXXX`` types (declared in ``ssrfun.v``) and the
+  :n:`if @term is @pattern then @term else @term` construct
+  (see :ref:`pattern_conditional_ssr`).  To use the
+  generalized form, turn off the |SSR| Boolean ``if`` notation using the command:
   ``Close Scope boolean_if_scope``.
 + The following two options can be unset to disable the incompatible
   rewrite syntax and allow reserved identifiers to appear in scripts.
@@ -191,9 +198,9 @@ construct differs from the latter in that
 + The pattern can be nested (deep pattern matching), in particular,
   this allows expression of the form:
 
-.. coqtop:: in
+.. coqdoc::
 
-  let: exist (x, y) p_xy := Hp in … .
+   let: exist (x, y) p_xy := Hp in … .
 
 + The destructured constructor is explicitly given in the pattern, and
   is used for type inference.
@@ -222,11 +229,7 @@ construct differs from the latter in that
 
 
 The ``let:`` construct is just (more legible) notation for the primitive
-|Gallina| expression
-
-.. coqtop:: in
-
-   match term with pattern => term end.
+|Gallina| expression :n:`match @term with @pattern => @term end`.
 
 The |SSR| destructuring assignment supports all the dependent
 match annotations; the full syntax is
@@ -286,28 +289,17 @@ assignment with a refutable pattern, adapted to the pure functional
 setting of |Gallina|, which lacks a ``Match_Failure`` exception.
 
 Like ``let:`` above, the ``if…is`` construct is just (more legible) notation
-for the primitive |Gallina| expression:
-
-.. coqtop:: in
-
-   match term with pattern => term | _ => term end.
+for the primitive |Gallina| expression
+:n:`match @term with @pattern => @term | _ => @term end`.
 
 Similarly, it will always be displayed as the expansion of this form
 in terms of primitive match expressions (where the default expression
 may be replicated).
 
 Explicit pattern testing also largely subsumes the generalization of
-the if construct to all binary data types; compare:
-
-.. coqtop:: in
-
-   if term is inl _ then term else term.
-
-and:
-
-.. coqtop:: in
-
-   if term then term else term.
+the ``if`` construct to all binary data types; compare
+:n:`if @term is inl _ then @term else @term` and
+:n:`if @term then @term else @term`.
 
 The latter appears to be marginally shorter, but it is quite
 ambiguous, and indeed often requires an explicit annotation
@@ -434,7 +426,7 @@ a functional constant, whose implicit arguments are prenex, i.e., the first
 As these prenex implicit arguments are ubiquitous and have often large
 display strings, it is strongly recommended to change the default
 display settings of |Coq| so that they are not printed (except after
-a ``Set Printing All command``). All |SSR| library files thus start
+a ``Set Printing All`` command). All |SSR| library files thus start
 with the incantation
 
 .. coqtop:: all undo
@@ -496,19 +488,10 @@ Definitions
 .. tacn:: pose
    :name: pose (ssreflect)
 
-This tactic allows to add a defined constant to a proof context.
-|SSR| generalizes this tactic in several ways. In particular, the
-|SSR| pose tactic supports *open syntax*: the body of the
-definition does not need surrounding parentheses. For instance:
-
-.. coqtop:: reset
-
-   From Coq Require Import ssreflect.
-   Set Implicit Arguments.
-   Unset Strict Implicit.
-   Unset Printing Implicit Defensive.
-   Lemma test : True.
-   Proof.
+   This tactic allows to add a defined constant to a proof context.
+   |SSR| generalizes this tactic in several ways. In particular, the
+   |SSR| pose tactic supports *open syntax*: the body of the
+   definition does not need surrounding parentheses. For instance:
 
 .. coqtop:: in
 
@@ -518,10 +501,18 @@ is a valid tactic expression.
 
 The pose tactic is also improved for the local definition of higher
 order terms. Local definitions of functions can use the same syntax as
-global ones. For example, the tactic ``pose`` supoprts parameters:
+global ones.
+For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters:
 
 .. example::
 
+   .. coqtop:: reset
+
+      From Coq Require Import ssreflect.
+      Set Implicit Arguments.
+      Unset Strict Implicit.
+      Unset Printing Implicit Defensive.
+
    .. coqtop:: all
 
       Lemma test : True.
@@ -631,7 +622,7 @@ where:
   surrounding the second :token:`term` are mandatory.
 + In the occurrence switch :token:`occ_switch`, if the first element of the
   list is a natural, this element should be a number, and not an Ltac
-  variable. The empty list {} is not interpreted as a valid occurrence
+  variable. The empty list ``{}`` is not interpreted as a valid occurrence
   switch.
 
 The tactic:
@@ -667,7 +658,7 @@ The tactic first tries to find a subterm of the goal matching
 the second :token:`term`
 (and its type), and stops at the first subterm it finds. Then
 the occurrences of this subterm selected by the optional :token:`occ_switch`
-are replaced by :token:`ident` and a definition ``ident := term``
+are replaced by :token:`ident` and a definition :n:`@ident := @term`
 is added to the
 context. If no :token:`occ_switch` is present, then all the occurrences are
 abstracted.
@@ -676,20 +667,20 @@ abstracted.
 Matching
 ````````
 
-The matching algorithm compares a pattern ``term`` with a subterm of the
+The matching algorithm compares a pattern :token:`term` with a subterm of the
 goal by comparing their heads and then pairwise unifying their
 arguments (modulo conversion). Head symbols match under the following
 conditions:
 
 
-+ If the head of ``term`` is a constant, then it should be syntactically
++ If the head of :token:`term` is a constant, then it should be syntactically
   equal to the head symbol of the subterm.
 + If this head is a projection of a canonical structure, then
   canonical structure equations are used for the matching.
 + If the head of term is *not* a constant, the subterm should have the
   same structure (λ abstraction,let…in structure …).
-+ If the head of ``term`` is a hole, the subterm should have at least as
-  many arguments as ``term``.
++ If the head of :token:`term` is a hole, the subterm should have at least as
+  many arguments as :token:`term`.
 
 .. example::
 
@@ -1082,7 +1073,7 @@ constants to the goal.
 
 Because they are tacticals, ``:`` and ``=>`` can be combined, as in
 
-.. coqtop: in
+.. coqtop:: in
 
    move: m le_n_m => p le_n_p.
 
@@ -1147,9 +1138,7 @@ induction on the top variable ``m`` with
    elim=> [|m IHm] n le_n.
 
 The general form of the localization tactical in is also best
-explained in terms of the goal stack:
-
-.. coqtop:: in
+explained in terms of the goal stack::
 
    tactic in a H1 H2 *.
 
@@ -1212,8 +1201,8 @@ product or a ``let…in``, and performs ``hnf`` otherwise.
 
 Of course this tactic is most often used in combination with the
 bookkeeping tacticals (see section :ref:`introduction_ssr` and :ref:`discharge_ssr`). These
-combinations mostly subsume the ``intros``, ``generalize``, ``revert``, ``rename``,
-``clear`` and ``pattern`` tactics.
+combinations mostly subsume the :tacn:`intros`, :tacn:`generalize`, :tacn:`revert`, :tacn:`rename`,
+:tacn:`clear` and :tacn:`pattern` tactics.
 
 
 The case tactic
@@ -1229,15 +1218,11 @@ The |SSR| case tactic has a special behavior on equalities. If the
 top assumption of the goal is an equality, the case tactic “destructs”
 it as a set of equalities between the constructor arguments of its
 left and right hand sides, as per the tactic injection. For example,
-``case`` changes the goal
-
-.. coqtop:: in
+``case`` changes the goal::
 
    (x, y) = (1, 2) -> G.
 
-into
-
-.. coqtop:: in
+into::
 
    x = 1 -> y = 2 -> G.
 
@@ -1289,9 +1274,7 @@ In fact the |SSR| tactic:
 .. tacn:: apply
    :name: apply (ssreflect)
 
-is a synonym for:
-
-.. coqtop:: in
+is a synonym for::
 
    intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top.
 
@@ -1322,18 +1305,14 @@ existential metavariables of sort Prop.
 
    Note that the last ``_`` of the tactic
    ``apply: (ex_intro _ (exist _ y _))``
-   represents a proof that ``y < 3``. Instead of generating the goal
-
-   .. coqtop:: in
+   represents a proof that ``y < 3``. Instead of generating the goal::
 
       0 < proj1_sig (exist (fun n : nat => n < 3) y ?Goal).
 
    the system tries to prove ``y < 3`` calling the trivial tactic.
    If it succeeds, let’s say because the context contains
    ``H : y < 3``, then the
-   system generates the following goal:
-
-   .. coqtop:: in
+   system generates the following goal::
 
       0 < proj1_sig (exist (fun n => n < 3) y H).
 
@@ -1579,7 +1558,7 @@ variables or assumptions from the goal.
 An :token:`s_item` can simplify the set of subgoals or the subgoals themselves:
 
 + ``//`` removes all the “trivial” subgoals that can be resolved by the
-  |SSR| tactic ``done`` described in :ref:`terminators_ssr`, i.e.,
+  |SSR| tactic :tacn:`done` described in :ref:`terminators_ssr`, i.e.,
   it executes ``try done``.
 + ``/=`` simplifies the goal by performing partial evaluation, as per the
   tactic ``simpl`` [#5]_.
@@ -1737,7 +1716,7 @@ new constant as an equation. The tactic:
 
 .. coqtop:: in
 
-  move En: (size l) => n.
+   move En: (size l) => n.
 
 where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and
 adds the fact ``En : size l = n`` to the context.
@@ -1745,7 +1724,7 @@ This is quite different from:
 
 .. coqtop:: in
 
-  pose n := (size l).
+   pose n := (size l).
 
 which generates a definition ``n := (size l)``. It is not possible to
 generalize or rewrite such a definition; on the other hand, it is
@@ -1834,7 +1813,7 @@ compact syntax:
 
 .. coqtop:: in
 
-  case: {2}_ / eqP.
+   case: {2}_ / eqP.
 
 where ``_`` is interpreted as ``(_ == _)`` since
 ``eqP T a b : reflect (a = b) (a == b)`` and reflect is a type family with
@@ -1999,19 +1978,9 @@ into a closing one (similar to now). Its general syntax is:
 .. tacn:: by @tactic
    :name: by
 
-The Ltac expression:
-
-.. coqtop:: in
-
-   by [@tactic | [@tactic | …].
-
-is equivalent to:
-
-.. coqtop:: in
-
-   [by @tactic | by @tactic | ...].
-
-and this form should be preferred to the former.
+The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to
+:n:`[by @tactic | by @tactic | ...]` and this form should be preferred
+to the former.
 
 In the script provided as example in section :ref:`indentation_ssr`, the
 paragraph corresponding to each sub-case ends with a tactic line prefixed
@@ -2021,20 +1990,13 @@ with a ``by``, like in:
 
    by apply/eqP; rewrite -dvdn1.
 
-The by tactical is implemented using the user-defined, and extensible
-done tactic. This done tactic tries to solve the current goal by some
-trivial means and fails if it doesn’t succeed. Indeed, the tactic
-expression:
-
-.. coqtop:: in
+.. tacn:: done
+   :name: done
 
-   by tactic.
-
-is equivalent to:
-
-.. coqtop:: in
-
-   tactic; done.
+The :tacn:`by` tactical is implemented using the user-defined, and extensible
+:tacn:`done` tactic. This :tacn:`done` tactic tries to solve the current goal by some
+trivial means and fails if it doesn’t succeed. Indeed, the tactic
+expression :n:`by @tactic` is equivalent to :n:`@tactic; done`.
 
 Conversely, the tactic
 
@@ -2735,7 +2697,7 @@ type classes inference.
   Full inference for ``ty``. The first subgoal demands a
   proof of such instantiated statement.
 
-+ coqtop::
++ .. coqdoc::
 
      have foo : ty := .
 
@@ -2817,21 +2779,23 @@ Another useful construct is reduction, showing that a particular case
 is in fact general enough to prove a general property. This kind of
 reasoning step usually starts with: “Without loss of generality, we
 can suppose that …”. Formally, this corresponds to the proof of a goal
-G by introducing a cut wlog_statement -> G. Hence the user shall
-provide a proof for both (wlog_statement -> G) -> G and
-wlog_statement -> G. However, such cuts are usually rather
+``G`` by introducing a cut ``wlog_statement -> G``. Hence the user shall
+provide a proof for both ``(wlog_statement -> G) -> G`` and
+``wlog_statement -> G``. However, such cuts are usually rather
 painful to perform by
-hand, because the statement wlog_statement is tedious to write by hand,
+hand, because the statement ``wlog_statement`` is tedious to write by hand,
 and sometimes even to read.
 
-|SSR| implements this kind of reasoning step through the without
-loss tactic, whose short name is ``wlog``. It offers support to describe
+|SSR| implements this kind of reasoning step through the :tacn:`without loss`
+tactic, whose short name is :tacn:`wlog`. It offers support to describe
 the shape of the cut statements, by providing the simplifying
 hypothesis and by pointing at the elements of the initial goals which
 should be generalized. The general syntax of without loss is:
 
 .. tacn:: wlog {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term
    :name: wlog
+.. tacv:: without loss {? suff } {? @clear_switch } {? @i_item } : {* @ident } / @term
+   :name: without loss
 
 where each :token:`ident` is a constant in the context
 of the goal. Open syntax is supported for :token:`term`.
@@ -2839,13 +2803,14 @@ of the goal. Open syntax is supported for :token:`term`.
 In its defective form:
 
 .. tacv:: wlog: / @term
+.. tacv:: without loss: / @term
 
 
 on a goal G, it creates two subgoals: a first one to prove the
 formula (term -> G) -> G and a second one to prove the formula
 term -> G.
 
-If the optional list of :token:`itent` is present
+If the optional list of :token:`ident` is present
 on the left side of ``/``, these constants are generalized in the
 premise (term -> G) of the first subgoal. By default bodies of local
 definitions are erased. This behavior can be inhibited by prefixing the
@@ -2858,9 +2823,9 @@ In the second subgoal, the tactic:
    move=> clear_switch i_item.
 
 is performed if at least one of these optional switches is present in
-the ``wlog`` tactic.
+the :tacn:`wlog` tactic.
 
-The ``wlog`` tactic is specially useful when a symmetry argument
+The :tacn:`wlog` tactic is specially useful when a symmetry argument
 simplifies a proof. Here is an example showing the beginning of the
 proof that quotient and reminder of natural number euclidean division
 are unique.
@@ -2881,9 +2846,10 @@ are unique.
      wlog: q1 q2 r1 r2 / q1 <= q2.
        by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith.
 
-The ``wlog suff`` variant is simpler, since it cuts wlog_statement instead
-of wlog_statement -> G. It thus opens the goals wlog_statement -> G
-and wlog_statement.
+The ``wlog suff`` variant is simpler, since it cuts ``wlog_statement`` instead
+of ``wlog_statement -> G``. It thus opens the goals
+``wlog_statement -> G``
+and ``wlog_statement``.
 
 In its simplest form the ``generally have : …`` tactic is equivalent to
 ``wlog suff : …`` followed by last first. When the ``have`` tactic is used
@@ -2922,7 +2888,7 @@ Advanced generalization
 The complete syntax for the items on the left hand side of the ``/``
 separator is the following one:
 
-.. tacv wlog … : {? @clear_switch | {? @  } @ident | ( {? @  } @ident := @c_pattern) } / @term
+.. tacv:: wlog … : {? @clear_switch | {? @  } @ident | ( {? @  } @ident := @c_pattern) } / @term
 
 Clear operations are intertwined with generalization operations. This
 helps in particular avoiding dependency issues while generalizing some
@@ -4684,9 +4650,11 @@ Note that the goal interpretation view mechanism supports both ``apply``
 and ``exact`` tactics. As expected, a goal interpretation view command
 exact/term should solve the current goal or it will fail.
 
-*Warning* Goal interpretation view tactics are *not* compatible with
-the bookkeeping tactical ``=>`` since this would be redundant with the
-``apply: term => _`` construction.
+.. warning::
+
+   Goal interpretation view tactics are *not* compatible with
+   the bookkeeping tactical ``=>`` since this would be redundant with the
+   ``apply: term => _`` construction.
 
 
 Boolean reflection
@@ -5390,6 +5358,8 @@ rewrite  see :ref:`rewriting_ssr`
 .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term
 .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
+.. tacv:: generally have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic }
+   :name: generally have
 
 forward  chaining see :ref:`structure_ssr`
 
@@ -5399,7 +5369,11 @@ forward  chaining see :ref:`structure_ssr`
 specializing see :ref:`structure_ssr`
 
 .. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+   :name: suff
+.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic }
+   :name: suffices
 .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
+.. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic }
 
 backchaining see :ref:`structure_ssr`
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 90ca0da43..29c2f8b81 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -971,7 +971,7 @@ quantification or an implication.
       move H0 before H.
 
 .. tacn:: rename @ident into @ident
-   :name: rename ... into ...
+   :name: rename
 
 This renames hypothesis :n:`@ident` into :n:`@ident` in the current context.
 The name of the hypothesis in the proof-term, however, is left unchanged.
diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py
index aeadce4c4..3ff00eaaf 100644
--- a/doc/tools/coqrst/repl/coqtop.py
+++ b/doc/tools/coqrst/repl/coqtop.py
@@ -41,10 +41,13 @@ class CoqTop:
                            the ansicolors module)
         :param args:       Additional arugments to coqtop.
         """
+        BOOT = True
+        if os.getenv('COQBOOT') == "no":
+            BOOT = False
         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.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color
         self.coqtop = None
 
     def __enter__(self):
diff --git a/parsing/extend.ml b/parsing/extend.ml
index f2af594ef..6805a96ed 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -116,7 +116,7 @@ and 'a rules =
 type 'a production_rule =
 | Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule
 
-type 'a single_extend_statment =
+type 'a single_extend_statement =
   string option *
   (** Level *)
   gram_assoc option *
@@ -124,6 +124,6 @@ type 'a single_extend_statment =
   'a production_rule list
   (** Symbol list with the interpretation function *)
 
-type 'a extend_statment =
+type 'a extend_statement =
   gram_position option *
-  'a single_extend_statment list
+  'a single_extend_statement list
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b78c35c26..6fdd9ea9b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -79,10 +79,10 @@ module type S =
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
   type coq_parsable
 
   val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
@@ -105,10 +105,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
 
   type coq_parsable = parsable * CLexer.lexer_state ref
 
@@ -207,9 +207,9 @@ let camlp5_verbosity silent f x =
 
 (** Grammar extensions *)
 
-(** NB: [extend_statment =
-         gram_position option * single_extend_statment list]
-    and [single_extend_statment =
+(** NB: [extend_statement =
+         gram_position option * single_extend_statement list]
+    and [single_extend_statement =
          string option * gram_assoc option * production_rule list]
     and [production_rule = symbol list * action]
 
@@ -263,7 +263,7 @@ let of_coq_extend_statement (pos, st) =
 type gram_reinit = gram_assoc * gram_position
 
 type extend_rule =
-| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule
+| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
 
 type ext_kind =
   | ByGrammar of extend_rule
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 36e5e420a..00ca53884 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -65,10 +65,10 @@ module type S =
   type symbol = Tok.t Gramext.g_symbol
   type action = Gramext.g_action
   type production_rule = symbol list * action
-  type single_extend_statment =
+  type single_extend_statement =
       string option * Gramext.g_assoc option * production_rule list
-  type extend_statment =
-      Gramext.position option * single_extend_statment list
+  type extend_statement =
+      Gramext.position option * single_extend_statement list
 
   type coq_parsable
 
@@ -264,7 +264,7 @@ type gram_reinit = gram_assoc * gram_position
 (** Type of reinitialization data *)
 
 val grammar_extend : 'a Gram.entry -> gram_reinit option ->
-  'a Extend.extend_statment -> unit
+  'a Extend.extend_statement -> unit
 (** Extend the grammar of Coq, without synchronizing it with the backtracking
     mechanism. This means that grammar extensions defined this way will survive
     an undo. *)
@@ -279,7 +279,7 @@ type 'a grammar_command
     marshallable. *)
 
 type extend_rule =
-| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statment -> extend_rule
+| ExtendRule : 'a Gram.entry * gram_reinit option * 'a extend_statement -> extend_rule
 
 type 'a grammar_extension = 'a -> GramState.t -> extend_rule list * GramState.t
 (** Grammar extension entry point. Given some ['a] and a current grammar state,
diff --git a/test-suite/misc/7595.sh b/test-suite/misc/7595.sh
new file mode 100755
index 000000000..836e354ee
--- /dev/null
+++ b/test-suite/misc/7595.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+set -e
+
+$coqc -R misc/7595 Test misc/7595/base.v
+$coqc -R misc/7595 Test misc/7595/FOO.v
diff --git a/test-suite/misc/7595/FOO.v b/test-suite/misc/7595/FOO.v
new file mode 100644
index 000000000..30c957d3b
--- /dev/null
+++ b/test-suite/misc/7595/FOO.v
@@ -0,0 +1,39 @@
+Require Import Test.base.
+
+Lemma dec_stable `{Decision P} : ¬¬P → P.
+Proof. firstorder. Qed.
+
+(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
+components is double negated, it will try to remove the double negation. *)
+Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
+  destruct dec as [H|H];
+  try match type of H with
+  | ¬¬_ => apply dec_stable in H
+  end.
+Tactic Notation "destruct_decide" constr(dec) :=
+  let H := fresh in destruct_decide dec as H.
+
+
+(** * Monadic operations *)
+Instance option_guard: MGuard option := λ P dec A f,
+  match dec with left H => f H | _ => None end.
+
+(** * Tactics *)
+Tactic Notation "case_option_guard" "as" ident(Hx) :=
+  match goal with
+  | H : context C [@mguard option _ ?P ?dec] |- _ =>
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
+  | |- context C [@mguard option _ ?P ?dec] =>
+    change (@mguard option _ P dec) with (λ A (f : P → option A),
+      match @decide P dec with left H' => f H' | _ => None end) in *;
+    destruct_decide (@decide P dec) as Hx
+  end.
+Tactic Notation "case_option_guard" :=
+  let H := fresh in case_option_guard as H.
+
+(* This proof failed depending on the name of the module. *)
+Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
+  P → (guard P; mx) = mx.
+Proof. intros. case_option_guard. reflexivity. contradiction. Qed.
diff --git a/test-suite/misc/7595/base.v b/test-suite/misc/7595/base.v
new file mode 100644
index 000000000..6a6b7b79d
--- /dev/null
+++ b/test-suite/misc/7595/base.v
@@ -0,0 +1,28 @@
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+Set Default Proof Using "Type".
+Export ListNotations.
+From Coq.Program Require Export Basics Syntax.
+Global Generalizable All Variables.
+
+(** * Type classes *)
+(** ** Decidable propositions *)
+(** This type class by (Spitters/van der Weegen, 2011) collects decidable
+propositions. *)
+Class Decision (P : Prop) := decide : {P} + {¬P}.
+Hint Mode Decision ! : typeclass_instances.
+Arguments decide _ {_} : simpl never, assert.
+
+(** ** Proof irrelevant types *)
+(** This type class collects types that are proof irrelevant. That means, all
+elements of the type are equal. We use this notion only used for propositions,
+but by universe polymorphism we can generalize it. *)
+Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
+Hint Mode ProofIrrel ! : typeclass_instances.
+
+Class MGuard (M : Type → Type) :=
+  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
+Arguments mguard _ _ _ !_ _ _ / : assert.
+Notation "'guard' P ; z" := (mguard P (λ _, z))
+  (at level 20, z at level 200, only parsing, right associativity) .
+Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
+  (at level 20, z at level 200, only parsing, right associativity) .