21 files changed, 159 insertions, 67 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7ebc2d8a4d..623debea23 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -4,6 +4,7 @@ stages:
   - docker
   - build
   - test
+  - deploy
 
 # some default values
 variables:
@@ -347,6 +348,35 @@ doc:refman:dune:
     paths:
       - _build/default/doc/sphinx_build/html
 
+doc:refman:deploy:
+  stage: deploy
+  environment:
+    name: deployment
+    url: https://coq.github.io/
+  only:
+    variables:
+      - $DOCUMENTATION_DEPLOY_KEY
+  dependencies:
+    - doc:refman:dune
+  before_script:
+    - which ssh-agent || ( apt-get update -y && apt-get install openssh-client -y )
+    - eval $(ssh-agent -s)
+    - echo "$DOCUMENTATION_DEPLOY_KEY" | tr -d '\r' | ssh-add - > /dev/null
+    - mkdir -p ~/.ssh
+    - chmod 700 ~/.ssh
+    - ssh-keyscan -t rsa github.com >> ~/.ssh/known_hosts
+    - git config --global user.name "coqbot"
+    - git config --global user.email "coqbot@users.noreply.github.com"
+  script:
+    - git clone git@github.com:coq/doc.git _deploy
+    - rm -rf _deploy/$CI_COMMIT_REF_NAME/refman # NB: won’t work if branch name has ‘/’ in it
+    - mkdir -p _deploy/$CI_COMMIT_REF_NAME
+    - cp -rv _build/default/doc/sphinx_build/html _deploy/$CI_COMMIT_REF_NAME/refman
+    - cd _deploy/$CI_COMMIT_REF_NAME/refman
+    - git add .
+    - git commit -m "User manual of branch “$CI_COMMIT_REF_NAME” at $CI_COMMIT_SHORT_SHA"
+    - git push # TODO: rebase and retry on failure
+
 doc:ml-api:odoc:
   <<: *dune-ci-template
   variables:
diff --git a/Makefile.dune b/Makefile.dune
index 78ecc4b056..e3a8a30bc2 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -91,9 +91,9 @@ ocheck: voboot
 	dune build $(DUNEOPT) @install --workspace=dev/dune-workspace.all
 
 trunk:
-	dune build $(DUNEOPT) --profile=ocaml408 @vodeps
+	dune build $(DUNEOPT) --profile=ocaml409 @vodeps
 	dune exec coq_dune $(BUILD_CONTEXT)/.vfiles.d
-	dune build $(DUNEOPT) --profile=ocaml408 coq.install coqide-server.install
+	dune build $(DUNEOPT) --profile=ocaml409 coq.install coqide-server.install
 
 ireport:
 	dune clean
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 67683902cd..962d2a94e3 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -51,7 +51,7 @@ function types over these data types.
 Consequently they also have a type. Because assuming simply that :math:`\Set`
 has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of
 |Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop`
-a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`.
+a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`.
 
 Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as
 booleans, natural numbers, as well as products, subsets and function
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 590d71b5f3..24645a8cc3 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -346,11 +346,46 @@ Navigation in the proof tree
 
          Goals are just existential variables and existential variables do not
          get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`.
+         You may also wrap this in an Ltac-definition like:
+
+         .. coqtop:: in
+
+            Ltac name_goal name := refine ?[name].
 
       .. seealso:: :ref:`existential-variables`
 
       .. example::
 
+         This first example uses the Ltac definition above, and the named goals
+         only serve for documentation.
+
+         .. coqtop:: all
+
+            Goal forall n, n + 0 = n.
+            Proof.
+            induction n; [ name_goal base | name_goal step ].
+            [base]: {
+
+         .. coqtop:: all
+
+            reflexivity.
+
+         .. coqtop:: in
+
+            }
+
+         .. coqtop:: all
+
+            [step]: {
+
+         .. coqtop:: all
+
+            simpl.
+            f_equal.
+            assumption.
+            }
+            Qed.
+
          This can also be a way of focusing on a shelved goal, for instance:
 
          .. coqtop:: all
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7eef504ea9..081fef07b9 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3307,12 +3307,29 @@ the conversion in hypotheses :n:`{+ @ident}`.
    :name: fold
 
    This tactic applies to any goal. The term :n:`@term` is reduced using the
-   ``red`` tactic. Every occurrence of the resulting :n:`@term` in the goal is
-   then replaced by :n:`@term`.
+   :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is
+   then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint
+   definition has been wrongfully unfolded, making the goal very hard to read.
+   On the other hand, when an unfolded function applied to its argument has been
+   reduced, the :tacn:`fold` tactic won't do anything.
 
-.. tacv:: fold {+ @term}
+   .. example::
+
+      .. coqtop:: all
+
+         Goal ~0=0.
+         unfold not.
+         Fail progress fold not.
+         pattern (0 = 0).
+         fold not.
+
+      .. coqtop:: none
+
+         Abort.
+
+   .. tacv:: fold {+ @term}
 
-   Equivalent to :n:`fold @term ; ... ; fold @term`.
+      Equivalent to :n:`fold @term ; ... ; fold @term`.
 
 .. tacn:: pattern @term
    :name: pattern
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index 0ad11d075f..e959e9b9e6 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -663,13 +663,8 @@ let init_entry_functions entry =
        entry.econtinue <- f; f lev bp a strm)
 
 let extend_entry ~warning entry position rules =
-  try
     let elev = Gramext.levels_of_rules ~warning entry position rules in
     entry.edesc <- Dlevels elev; init_entry_functions entry
-  with Plexing.Error s ->
-    Printf.eprintf "Lexer initialization error:\n- %s\n" s;
-    flush stderr;
-    failwith "Grammar.extend"
 
 (* Deleting a rule *)
 
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index f99a3c2480..fce5445ad8 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -4,8 +4,6 @@
 
 type pattern = string * string
 
-exception Error of string
-
 type location_function = int -> Loc.t
 type 'te lexer_func = char Stream.t -> 'te Stream.t * location_function
 
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index eed4082e00..6139dc4020 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -19,9 +19,6 @@ type pattern = string * string
 -      The way tokens patterns are interpreted to parse tokens is done
        by the lexer, function [tok_match] below. *)
 
-exception Error of string
-    (** A lexing error exception to be used by lexers. *)
-
 (** Lexer type *)
 
 type 'te lexer =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 02f38e7214..886d6b1feb 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -222,6 +222,10 @@ let lookup_constant kn env =
 let lookup_mind kn env =
   fst (Mindmap_env.find kn env.env_globals.env_inductives)
 
+let mind_context env mind =
+  let mib = lookup_mind mind env in
+  Declareops.inductive_polymorphic_context mib
+
 let lookup_mind_key kn env =
   Mindmap_env.find kn env.env_globals.env_inductives
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8d5bd85b94..a9e0717559 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -246,6 +246,10 @@ val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
    raises [Not_found] if the required path is not found *)
 val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
+(** The universe context associated to the inductive, empty if not
+    polymorphic *)
+val mind_context : env -> MutInd.t -> Univ.AUContext.t
+
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
 val polymorphic_pind : pinductive -> env -> bool
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 9bb848c6a4..674d7a2a91 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -536,9 +536,13 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr
   let record_info = match isrecord with
   | Some (Some rid) ->
     let is_record pkt =
-      List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim
-      && Array.length pkt.mind_consnames == 1
-      && pkt.mind_consnrealargs.(0) > 0
+      if Array.length pkt.mind_consnames != 1 then
+        user_err ~hdr:"build_inductive"
+          Pp.(str "Primitive records must have exactly one constructor.")
+      else if pkt.mind_consnrealargs.(0) = 0 then
+        user_err ~hdr:"build_inductive"
+          Pp.(str "Primitive records must have at least one constructor argument.")
+      else List.exists (Sorts.family_equal Sorts.InType) pkt.mind_kelim
     in
     (** The elimination criterion ensures that all projections can be defined. *)
     if Array.for_all is_record packets then
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 04a17f7b08..414c443c4e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -88,17 +88,11 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind ((mi,_i) as ind1) , Aind ind2 ->
     if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
-      if Environ.polymorphic_ind ind1 env then
-        let mib = Environ.lookup_mind mi env in
-	let ulen = 
-          match mib.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
-          | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
-          | Declarations.Cumulative_ind cumi -> 
-            Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
-        in
+      let ulen = Univ.AUContext.size (Environ.mind_context env mi) in
+      if ulen = 0 then
+        conv_stack env k stk1 stk2 cu
+      else
         match stk1 , stk2 with
-	| [], [] -> assert (Int.equal ulen 0); cu
         | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
           assert (ulen <= nargs args1);
           assert (ulen <= nargs args2);
@@ -110,8 +104,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
           conv_arguments env ~from:ulen k args1 args2
 	    (conv_stack env k stk1' stk2' cu)
         | _, _ -> assert false (* Should not happen if problem is well typed *)
-      else
-	conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | Aid ik1, Aid ik2 ->
     if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg
index 4ddaeb49fd..d1c7a23e99 100644
--- a/plugins/ssrmatching/g_ssrmatching.mlg
+++ b/plugins/ssrmatching/g_ssrmatching.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.             *)
+
 {
 
 open Ltac_plugin
diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli
index 588a1a3eac..65ea3f79c8 100644
--- a/plugins/ssrmatching/g_ssrmatching.mli
+++ b/plugins/ssrmatching/g_ssrmatching.mli
@@ -1,5 +1,14 @@
-(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.             *)
 
 open Genarg
 open Ssrmatching
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f58cce41cc..6d9e3230a4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -197,32 +197,19 @@ let keep_true_projections projs kinds =
   let filter (p, (_, b)) = if b then Some p else None in
   List.map_filter filter (List.combine projs kinds)
 
-let cs_pattern_of_constr env t =
+let rec cs_pattern_of_constr env t =
   match kind t with
-      App (f,vargs) ->
-	begin
-	  try Const_cs (global_of_constr f) , None, Array.to_list vargs
-          with
-          | Not_found when isProj f ->
-              let p, c = destProj f in
-              let { Environ.uj_type = ty } = Typeops.infer env c in
-              let _, params = Inductive.find_rectype env ty in
-              Const_cs (ConstRef (Projection.constant p)), None,
-              params @ [c] @ Array.to_list vargs
-          | e when CErrors.noncritical e -> raise Not_found
-	end
-    | Rel n -> Default_cs, Some n, []
-    | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
-    | Proj (p, c) ->
-      let { Environ.uj_type = ty } = Typeops.infer env c in
-      let _, params = Inductive.find_rectype env ty in
-      Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
-    | Sort s -> Sort_cs (Sorts.family s), None, []
-    | _ ->
-	begin
-	  try Const_cs (global_of_constr t) , None, []
-          with e when CErrors.noncritical e -> raise Not_found
-	end
+  | App (f,vargs) ->
+    let patt, n, args = cs_pattern_of_constr env f in
+    patt, n, args @ Array.to_list vargs
+  | Rel n -> Default_cs, Some n, []
+  | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
+  | Proj (p, c) ->
+    let { Environ.uj_type = ty } = Typeops.infer env c in
+    let _, params = Inductive.find_rectype env ty in
+    Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
+  | Sort s -> Sort_cs (Sorts.family s), None, []
+  | _ -> Const_cs (global_of_constr t) , None, []
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5..f41706c35e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4522,8 +4522,11 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
+      let avoid = match eqname with
+        | Some {CAst.v=IntroIdentifier id} -> Id.Set.singleton id
+        | _ -> Id.Set.empty in
       let x = id_of_name_using_hdchar env evd t Anonymous in
-      new_fresh_id Id.Set.empty x gl in
+      new_fresh_id avoid x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
       isrec with_evars info_arg elim id arg t inhyps cls
diff --git a/test-suite/bugs/closed/bug_9494.v b/test-suite/bugs/closed/bug_9494.v
new file mode 100644
index 0000000000..a0b8383d16
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9494.v
@@ -0,0 +1,10 @@
+Lemma foo (a : nat) : True.
+Proof.
+destruct a eqn:n; exact I.
+Qed.
+
+Set Mangle Names.
+Lemma foo2 (a : nat) : True.
+Proof.
+let N := fresh in destruct a eqn:N; exact I.
+Qed.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index cdbe444e5b..e933f08735 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -256,7 +256,7 @@ let rec discard_to_dot () =
   try
     Pcoq.Entry.parse parse_to_dot top_buffer.tokens
   with
-    | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot ()
+    | CLexer.Error.E _ -> discard_to_dot ()
     | e when CErrors.noncritical e -> ()
 
 let read_sentence ~state input =
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 71770a21ca..42b313f200 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -28,7 +28,6 @@ exception EvaluatedError of Pp.t * exn option
 let explain_exn_default = function
   (* Basic interaction exceptions *)
   | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
-  | Gramlib.Plexing.Error txt -> hov 0 (str "Syntax error: " ++ str txt ++ str ".")
   | CLexer.Error.E err -> hov 0 (str (CLexer.Error.to_string err))
   | Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
   | Out_of_memory -> hov 0 (str "Out of memory.")
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6642d04c98..b4dd7d06b5 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -921,15 +921,15 @@ let obligation_hook prg obl num auto ctx' _ gr =
     | (true, Evar_kinds.Define true) ->
        if not transparent then err_not_transp ()
     | _ -> ()
-in
+  in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let inst, ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let evd = Evd.from_env (Global.env ()) in
-      let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
-      Univ.Instance.empty, Evd.evar_universe_context ctx'
+      let ctx = UState.make (Global.universes ()) in
+      let ctx' = UState.merge_subst ctx (UState.subst ctx') in
+      Univ.Instance.empty, ctx'
     else
       (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
       let uctx = UState.context ctx' in
diff --git a/vernac/record.ml b/vernac/record.ml
index 1b7b828f47..ed5edb7e3b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -414,9 +414,15 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
       mind_entry_lc = [type_constructor] }
   in
   let blocks = List.mapi mk_block record_data in
+  let primitive =
+    !primitive_flag &&
+    List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+    (* will warn_non_primitive_record in declare_projections if we try
+       to declare a 0-field record *)
+  in
   let mie =
     { mind_entry_params = params;
-      mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
+      mind_entry_record = Some (if primitive then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = blocks;
       mind_entry_private = None;