6 files changed, 57 insertions, 70 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1669145d9b..bb1aa81a73 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-10-04-V1"
+  CACHEKEY: "bionic_coq-V2018-10-22-V1"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index f257c62dd3..41e1d1a937 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-04-V2"
+# CACHEKEY: "bionic_coq-V2018-10-22-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `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 odoc.1.2.0" \
+ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.3.0" \
     CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
diff --git a/man/coq-interface.1 b/man/coq-interface.1
deleted file mode 100644
index ee013d952e..0000000000
--- a/man/coq-interface.1
+++ /dev/null
@@ -1,37 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coq\-interface \- Customized Coq toplevel to make user interfaces
-
-
-.SH SYNOPSIS
-.B coq-interface
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B coq-interface
-is a Coq customized toplevel system for Coq containing some modules
-useful for the graphical interface. This program is not for the casual
-user.
-
-.SH OPTIONS
-
-.TP
-.B \-h
-Help. Will give you the complete list of options accepted by
-coq-interface (the same as coqtop).
-
-.SH SEE ALSO
-
-.BR coqc (1),
-.BR coqdep (1),
-.BR coqtop (1),
-.BR coq\-parser (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/man/coq-parser.1 b/man/coq-parser.1
deleted file mode 100644
index 23dc820193..0000000000
--- a/man/coq-parser.1
+++ /dev/null
@@ -1,30 +0,0 @@
-.TH COQ 1 "April 25, 2001"
-
-.SH NAME
-coq\-parser \- Coq parser
-
-
-.SH SYNOPSIS
-.B coq\-parser
-[
-.B options
-]
-
-.SH DESCRIPTION
-
-.B parser
-is a program reading Coq proof developments and outputing them in the
-structured format given in the INRIA technical report RT154. This
-program is not for the casual user.
-
-.SH SEE ALSO
-
-.BR coq\-interface (1),
-.BR coqc (1),
-.BR coqtop (1),
-.BR coqdep (1).
-.br
-.I
-The Coq Reference Manual.
-.I
-The Coq web site: http://coq.inria.fr
diff --git a/man/dune b/man/dune
new file mode 100644
index 0000000000..359e780545
--- /dev/null
+++ b/man/dune
@@ -0,0 +1,10 @@
+(install
+ (section man)
+ (package coq)
+ (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1))
+
+(install
+ (section man)
+ (package coqide)
+ (files coqide.1))
+
diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v
new file mode 100644
index 0000000000..b10569499e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8785.v
@@ -0,0 +1,44 @@
+Universe u v w.
+Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := .
+
+Inductive FiniteT : Type -> Prop :=
+  | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T)
+  | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X ->
+    invertible f -> FiniteT Y.
+
+Set Printing Universes.
+
+Axiom a : False.
+(*
+Constraint v <= u.
+Constraint v <= w.
+*)
+Lemma finite_subtype: forall (X:Type) (P:X->Prop),
+  FiniteT X -> (forall x:X, P x \/ ~ P x) ->
+  FiniteT {x:X | P x}.
+Proof.
+intros.
+induction H.
+
+destruct (H0 None).
+elim a.
+
+pose (g := fun (x:{x:T | P (Some x)}) =>
+  match x return {x:option T | P x} with
+    | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+pose (g := fun (x:{x:X | P (f x)}) =>
+  match x with
+  | exist _ x0 i => exist (fun x:Y => P x) (f x0) i
+  end).
+apply bij_finite with _ g.
+apply IHFiniteT.
+intro; apply H0.
+elim a.
+
+Qed.