27 files changed, 205 insertions, 62 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8b43d975a..b47494d3a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -40,6 +40,11 @@ before_script:
   - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi
   - ln -s $(readlink -f .opamcache) ~/.opam
 
+  # the default repo in this docker image is a local directory
+  # at the time of 4aaeb8abf it lagged behind the official
+  # repository such that camlp5 7.01 was not available
+  - opam repository set-url default https://opam.ocaml.org
+  - opam update
   - opam switch ${COMPILER}
   - eval $(opam config env)
   - opam config list
diff --git a/.travis.yml b/.travis.yml
index 3cd7fdf5e..e40568995 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -64,7 +64,6 @@ matrix:
   allow_failures:
   - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
   - env: TEST_TARGET="ci-geocoq"
-  - env: TEST_TARGET="ci-fiat-parsers"
 
   include:
     # Full Coq test-suite with two compilers
diff --git a/API/API.mli b/API/API.mli
index f2324bb44..19726b52f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4625,6 +4625,7 @@ sig
   val get_current_proof_name : unit -> Names.Id.t
   [@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
 
+  val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
 end
 
 module Clenv :
@@ -5400,6 +5401,8 @@ sig
   val pp_hints_path : hints_path -> Pp.std_ppcmds
   val glob_hints_path :
     Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen
+  val run_hint : hint ->
+    ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
   val typeclasses_db : hint_db_name
   val add_hints_init : (unit -> unit) -> unit
   val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit
diff --git a/Makefile b/Makefile
index 2e49c84b5..8d9b657d1 100644
--- a/Makefile
+++ b/Makefile
@@ -42,9 +42,9 @@
 # to communicate between make sub-calls (in Win32, 8kb max per env variable,
 # 32kb total)
 
-# !! Before using FIND_VCS_CLAUSE, please read how you should in the !!
-# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt         !!
-FIND_VCS_CLAUSE:='(' \
+# !! Before using FIND_SKIP_DIRS, please read how you should in the !!
+# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt         !!
+FIND_SKIP_DIRS:='(' \
   -name '{arch}' -o \
   -name '.svn' -o \
   -name '_darcs' -o \
@@ -55,25 +55,23 @@ FIND_VCS_CLAUSE:='(' \
   -name '_build' -o \
   -name '_build_ci' -o \
   -name 'coq-makefile' -o \
-  -name '.opamcache' \
+  -name '.opamcache' -o \
+  -name '.coq-native' \
 ')' -prune -o
 
 define find
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||')
+ $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||')
 endef
 
 define findindir
- $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||')
-endef
-
-define findx
- $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||')
+ $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||')
 endef
 
 ## Files in the source tree
 
 LEXFILES := $(call find, '*.mll')
-export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack')
+export MLLIBFILES := $(call find, '*.mllib')
+export MLPACKFILES := $(call find, '*.mlpack')
 export ML4FILES := $(call find, '*.ml4')
 export CFILES := $(call findindir, 'kernel/byterun', '*.c')
 
@@ -97,11 +95,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)
 
 ## More complex file lists
 
-define diff
- $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f)))
-endef
-
-export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES))
+export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML))
 export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI))
 
 include Makefile.common
@@ -139,6 +133,36 @@ Then, you may want to consider whether you want to restore the autosaves)
 #run.
 endif
 
+# Check that every compiled file around has a known source file.
+# This should help preventing weird compilation failures caused by leftover
+# compiled files after deleting or moving some source files.
+
+ifndef ACCEPT_ALIEN_VO
+EXISTINGVO:=$(call find, '*.vo')
+KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v'))
+ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO))
+ifdef ALIENVO
+$(error Leftover compiled Coq files without known sources: $(ALIENVO); \
+remove them first, for instance via 'make voclean' \
+(or skip this check via 'make ACCEPT_ALIEN_VO=1'))
+endif
+endif
+
+ifndef ACCEPT_ALIEN_OBJ
+EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa')
+KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \
+ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp))
+KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \
+ $(MLIFILES:.mli=.cmi) \
+ $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma
+ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS))
+ifdef ALIENOBJS
+$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \
+remove them first, for instance via 'make clean' \
+(or skip this check via 'make ACCEPT_ALIEN_OBJ=1'))
+endif
+endif
+
 # Apart from clean and tags, everything will be done in a sub-call to make
 # on Makefile.build. This way, we avoid doing here the -include of .d :
 # since they trigger some compilations, we do not want them for a mere clean.
@@ -218,7 +242,7 @@ archclean: clean-ide optclean voclean
 optclean:
 	rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN)
 	rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT)
-	find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
+	find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f
 
 clean-ide:
 	rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE)
@@ -231,7 +255,7 @@ ml4clean:
 	rm -f $(GENML4FILES)
 
 depclean:
-	find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f
+	find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f
 
 cacheclean:
 	find theories plugins test-suite -name '.*.aux' -delete
diff --git a/Makefile.build b/Makefile.build
index e3316df91..7961092fa 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -151,7 +151,7 @@ endif
 # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d).
 
 DEPENDENCIES := \
- $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES))
+ $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES))
 
 -include $(DEPENDENCIES)
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 656030543..4b3b44875 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -85,8 +85,8 @@
 ########################################################################
 # fiat_parsers
 ########################################################################
-: ${fiat_parsers_CI_BRANCH:=trunk__API}
-: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git}
+: ${fiat_parsers_CI_BRANCH:=master}
+: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}
 
 ########################################################################
 # fiat_crypto
diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt
index fefcb0937..f3fc13e96 100644
--- a/dev/doc/build-system.dev.txt
+++ b/dev/doc/build-system.dev.txt
@@ -74,25 +74,25 @@ The Makefile is separated in several files :
 - Makefile.doc : specific rules for compiling the documentation.
 
 
-FIND_VCS_CLAUSE
+FIND_SKIP_DIRS
 ---------------
 
-The recommended style of using FIND_VCS_CLAUSE is for example
+The recommended style of using FIND_SKIP_DIRS is for example
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print
 
 1)
 The parentheses even in the one-criteria case is so that if one adds
 other conditions, e.g. change the first example to the second
 
- find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
 
 one is not tempted to write
 
- find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print
+ find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
 
-because this will not necessarily work as expected; $(FIND_VCS_CLAUSE)
+because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
 ends with an -or, and how it combines with what comes later depends on
 operator precedence and all that. Much safer to override it with
 parentheses.
@@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why.
 You are used to write:
  find . -name '*.example'
 and it works fine. But the following will not:
- find . $(FIND_VCS_CLAUSE) -name '*.example'
-it will also list things directly matched by FIND_VCS_CLAUSE
+ find . $(FIND_SKIP_DIRS) -name '*.example'
+it will also list things directly matched by FIND_SKIP_DIRS
 (directories we want to prune, in which we don't want to find
 anything). C'est subtil... Il y a effectivement un -print implicite à
 la fin, qui fait que la commande habituelle sans print fonctionne
 bien, mais dès que l'on introduit d'autres commandes dans le lot (le
--prune de FIND_VCS_CLAUSE), ça se corse à cause d'histoires de
+-prune de FIND_SKIP_DIRS), ça se corse à cause d'histoires de
 parenthèses du -print implicite par rapport au parenthésage dans la
 forme recommandée d'utilisation:
 
diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex
index 349164948..337b9226d 100644
--- a/dev/doc/naming-conventions.tex
+++ b/dev/doc/naming-conventions.tex
@@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix
 {forall x y:D, op (op' x y) = op' x (op y)}
 
 \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent}
-{forall x:D, op x n = x}
+{forall x:D, op x x = x}
 
 \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent}
 {forall x:D, op (op x) = op x}
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 7ffe25225..b93ca2957 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -6,7 +6,7 @@
 
 This chapter explains how proofs can be asynchronously processed by Coq.
 This feature improves the reactivity of the system when used in interactive
-mode via CoqIDE.  In addition to that, it allows Coq to take advantage of
+mode via CoqIDE. In addition, it allows Coq to take advantage of
 parallel hardware when used as a batch compiler by decoupling the checking
 of statements and definitions from the construction and checking of proofs
 objects.
@@ -22,7 +22,12 @@ For example, in interactive mode, some errors coming from the kernel of Coq
 are signaled late.  The type of errors belonging to this category
 are universe inconsistencies.
 
-Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
+At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
+
+Finally, asynchronous processing is disabled when running CoqIDE in Windows. The
+current implementation of the feature is not stable on Windows. It can be
+enabled, as described below at \ref{interactivecaveats}, though doing so is not
+recommended.
 
 \section{Proof annotations}
 
@@ -112,6 +117,7 @@ the kernel to check all the proof objects, one has to click the button
 with the gears. Only then are all the universe constraints checked.
 
 \subsubsection{Caveats}
+\label{interactivecaveats}
 
 The number of worker processes can be increased by passing CoqIDE the
 \texttt{-async-proofs-j $n$} flag.  Note that the memory consumption
@@ -120,7 +126,8 @@ the master process. Also note that increasing the number of workers may
 reduce the reactivity of the master process to user commands.
 
 To disable this feature, one can pass the \texttt{-async-proofs off} flag to
-CoqIDE.
+CoqIDE. Conversely, on Windows, where the feature is disabled by default,
+pass the \texttt{-async-proofs on} flag to enable it.
 
 Proofs that are known to take little time to process are not delegated to a
 worker process.  The threshold can be configure with \texttt{-async-proofs-delegation-threshold}.  Default is 0.03 seconds.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 48f82f2d9..48048b7a0 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -591,5 +591,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/AdmitAxiom.v
     theories/Compat/Coq85.v
     theories/Compat/Coq86.v
+    theories/Compat/Coq87.v
   </dd>
 </dl>
diff --git a/ide/coq.ml b/ide/coq.ml
index 8ecdf9caa..0fe831ab3 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -366,7 +366,14 @@ let bind_self_as f =
 (** This launches a fresh handle from its command line arguments. *)
 let spawn_handle args respawner feedback_processor =
   let prog = coqtop_path () in
-  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
+  let async_default =
+    (* disable async processing by default in Windows *)
+    if List.mem Sys.os_type ["Win32"; "Cygwin"] then
+      "off"
+    else
+      "on"
+  in
+  let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in
   let env =
     match !Flags.ideslave_coqtop_flags with
     | None -> None
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f360fb192..c9fc3aa4f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -664,11 +664,11 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
     | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
         let e = make_letins letins (aux subst' infos c') in
-        let (loc,(na,bk,t)) = a in
+        let (_loc,(na,bk,t)) = a in
         CAst.make ?loc @@ GProd (na,bk,t,e)
     | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let a,letins = snd (Option.get binderopt) in
-        let (loc,(na,bk,t)) = a in
+        let (_loc,(na,bk,t)) = a in
         CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
     (* Two special cases to keep binder name synchronous with BinderType *)
     | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
diff --git a/lib/flags.ml b/lib/flags.ml
index 5d9d9dcf5..0bce22f58 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,7 +106,7 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = VOld | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current
 
 let compat_version = ref Current
 
@@ -120,6 +120,9 @@ let version_compare v1 v2 = match v1, v2 with
   | V8_6, V8_6 -> 0
   | V8_6, _ -> -1
   | _, V8_6 -> 1
+  | V8_7, V8_7 -> 0
+  | V8_7, _ -> -1
+  | _, V8_7 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
@@ -129,6 +132,7 @@ let pr_version = function
   | VOld -> "old"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
+  | V8_7 -> "8.7"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index e63f1ec26..eb4c37a54 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,7 +77,7 @@ val raw_print : bool ref
 (* Univ print flag, never set anywere. Maybe should belong to Univ? *)
 val univ_print : bool ref
 
-type compat_version = VOld | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/lib/profile.ml b/lib/profile.ml
index b66916185..0bc226a45 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -85,6 +85,9 @@ let init_alloc = ref 0.0
 let reset_profile () = List.iter reset_record !prof_table
 
 let init_profile () =
+  (* We test Flags.profile as a way to support declaring profiled
+     functions in plugins *)
+  if !prof_table <> [] || Flags.profile then begin
   let outside = create_record () in
   stack := [outside];
   last_alloc := get_alloc ();
@@ -92,6 +95,7 @@ let init_profile () =
   init_time := get_time ();
   outside.tottime <- - !init_time;
   outside.owntime <- - !init_time
+  end
 
 let ajoute n o =
   o.owntime <- o.owntime + n.owntime;
@@ -317,15 +321,15 @@ let adjust_time ov_bc ov_ad e =
      owntime = e.owntime - int_of_float (ad_imm +. bc_imm) }
 
 let close_profile print =
-  let dw = spent_alloc () in
-  let t = get_time () in
-  match !stack with
-    | [outside] ->
-	outside.tottime <- outside.tottime + t;
-	outside.owntime <- outside.owntime + t;
-	ajoute_ownalloc outside dw;
-	ajoute_totalloc outside dw;
-	if !prof_table <> [] then begin
+  if !prof_table <> [] then begin
+      let dw = spent_alloc () in
+      let t = get_time () in
+      match !stack with
+      | [outside] ->
+	  outside.tottime <- outside.tottime + t;
+	  outside.owntime <- outside.owntime + t;
+	  ajoute_ownalloc outside dw;
+	  ajoute_totalloc outside dw;
 	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
 	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
 	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
@@ -346,8 +350,8 @@ let close_profile print =
 	  in
 	  if print then format_profile updated_data;
 	  init_profile ()
-	end
-    | _ -> failwith "Inconsistency"
+      | _ -> failwith "Inconsistency"
+    end
 
 let print_profile () = close_profile true
 
@@ -358,9 +362,6 @@ let declare_profile name =
   prof_table := (name,e)::!prof_table;
   e
 
-(* Default initialization, may be overridden *)
-let _ = init_profile ()
-
 (******************************)
 (* Entry points for profiling *)
 let profile1 e f a =
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f1bcde2f3..a4c2bcd88 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -120,7 +120,6 @@ let rec mgu = function
       mgu (a, a'); mgu (b, b')
   | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
   | Tvar i, Tvar j when Int.equal i j -> ()
   | Tvar' i, Tvar' j when  Int.equal i j -> ()
@@ -1052,6 +1051,7 @@ let rec simpl o = function
   | MLmagic(MLcase(typ,e,br)) ->
      let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
      simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
   | MLmagic(MLexn _ as e) -> e
   | a -> ast_map (simpl o) a
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6cc9d3d55..3fc2fc31b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1143,7 +1143,7 @@ module Search = struct
         let res =
           if j = 0 then tclUNIT ()
           else tclDISPATCH
-                 (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j))))
+                 (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j'))))
         in
         let finish nestedshelf sigma =
           let filter ev =
diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v
new file mode 100644
index 000000000..f140939cc
--- /dev/null
+++ b/test-suite/bugs/closed/4844.v
@@ -0,0 +1,47 @@
+
+(* Bug report 4844 (and 4824):
+   The Haskell extraction was erroneously considering [Any] and
+   [()] as convertible ([Tunknown] an [Tdummy] internally). *)
+
+(* A value with inner logical parts.
+   Its extracted type will be [Sum () ()]. *)
+
+Definition semilogic : True + True := inl I.
+
+(* Higher-order record, whose projection [ST] isn't expressible
+   as an Haskell (or OCaml) type. Hence [ST] is extracted as the
+   unknown type [Any] in Haskell. *)
+
+Record SomeType := { ST : Type }.
+
+Definition SomeTrue := {| ST := True |}.
+
+(* A first version of the issue:
+  [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce
+  is required to cast [semilogic] into [abstrSum SomeTrue]. *)
+
+Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type.
+
+Definition semilogic' : abstrSum SomeTrue := semilogic.
+
+(* A deeper version of the issue.
+   In the previous example, the extraction could have reduced
+   [abstrSum SomeTrue] into [True+True], solving the issue.
+   It might do so in future versions. But if we put an inductive
+   in the way, a reduction isn't helpful. *)
+
+Inductive box (t : SomeType) := Box : ST t + ST t -> box t.
+
+Definition boxed_semilogic : box SomeTrue :=
+ Box SomeTrue semilogic.
+
+Require Extraction.
+Extraction Language Haskell.
+Recursive Extraction semilogic' boxed_semilogic.
+(* Warning! To fully check that this bug is still closed,
+   you should run ghc on the extracted code:
+
+Extraction "bug4844.hs" semilogic' boxed_semilogic.
+ghc bug4844.hs
+
+*)
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
index f46460886..34061ddd6 100644
--- a/theories/Compat/Coq86.v
+++ b/theories/Compat/Coq86.v
@@ -7,5 +7,7 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.6 *)
+Require Export Coq.Compat.Coq87.
+
 Require Export Coq.extraction.Extraction.
 Require Export Coq.funind.FunInd.
diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v
new file mode 100644
index 000000000..61e911678
--- /dev/null
+++ b/theories/Compat/Coq87.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.7 *)
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index b1c0fdaa2..3e7664929 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -654,19 +654,19 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
 
   Lemma xelements_bits_lt_1 : forall p p0 q m v,
      List.In (p0,v) (xelements m (append p (xO q))) -> E.bits_lt p0 p.
-  Proof.
+  Proof using.
   intros.
   generalize (xelements_complete _ _ _ _ H); clear H; intros.
-  revert p0 q m v H.
+  revert p0 H.
   induction p; destruct p0; simpl; intros; eauto; try discriminate.
   Qed.
 
   Lemma xelements_bits_lt_2 : forall p p0 q m v,
      List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0.
-  Proof.
+  Proof using.
   intros.
   generalize (xelements_complete _ _ _ _ H); clear H; intros.
-  revert p0 q m v H.
+  revert p0 H.
   induction p; destruct p0; simpl; intros; eauto; try discriminate.
   Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ce49877e4..967b68d36 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -602,6 +602,14 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_div: forall a b, b~=0 ->
+ a mod b / b == 0.
+Proof.
+ intros a b Hb.
+ rewrite div_small_iff by assumption.
+ auto using mod_always_pos.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index ca6197002..a9077127e 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -650,6 +650,14 @@ Proof.
  apply div_mod; order.
 Qed.
 
+Lemma mod_div: forall a b, b~=0 ->
+ a mod b / b == 0.
+Proof.
+ intros a b Hb.
+ rewrite div_small_iff by assumption.
+ auto using mod_bound_or.
+Qed.
+
 (** A last inequality: *)
 
 Theorem div_mul_le:
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 46c36015d..bbb8ad5ae 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -622,6 +622,14 @@ Proof.
  apply quot_rem; order.
 Qed.
 
+Lemma rem_quot: forall a b, b~=0 ->
+ a rem b ÷ b == 0.
+Proof.
+ intros a b Hb.
+ rewrite quot_small_iff by assumption.
+ auto using rem_bound_abs.
+Qed.
+
 (** A last inequality: *)
 
 Theorem quot_mul_le:
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 55fc90f21..fa1ddf56f 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -508,6 +508,13 @@ Qed.
 (** Unfortunately, the previous result isn't always true on negative numbers.
     For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *)
 
+Lemma Zmod_div : forall a b, a mod b / b = 0.
+Proof.
+ intros a b.
+ zero_or_not b.
+ auto using Z.mod_div.
+Qed.
+
 (** A last inequality: *)
 
 Theorem Zdiv_mult_le:
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index f61416dde..326ef5471 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -127,7 +127,8 @@ let init_ocaml_path () =
     List.iter add_subdir Coq_config.all_src_dirs
 
 let get_compat_version ?(allow_old = true) = function
-  | "8.7" -> Flags.Current
+  | "8.8" -> Flags.Current
+  | "8.7" -> Flags.V8_7
   | "8.6" -> Flags.V8_6
   | "8.5" -> Flags.V8_5
   | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 08c235023..515552fe7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -209,6 +209,7 @@ let add_compat_require v =
   match v with
   | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
   | Flags.V8_6 -> add_require "Coq.Compat.Coq86"
+  | Flags.V8_7 -> add_require "Coq.Compat.Coq87"
   | Flags.VOld | Flags.Current -> ()
 
 let compile_list = ref ([] : (bool * string) list)
@@ -613,6 +614,7 @@ let parse_args arglist =
   with any -> fatal_error any
 
 let init_toplevel arglist =
+  Profile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in