12 files changed, 140 insertions, 27 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 9e87d2ca7..3a762b42a 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -53,6 +53,9 @@
 /doc/             @maximedenes
 # Secondary maintainer @silene @Zimmi48
 
+/doc/tools/coqrst/ @maximedenes
+# Secondary maintainer @cpitclaudel
+
 /man/             @silene
 # Secondary maintainer @maximedenes
 
diff --git a/INSTALL.ide b/INSTALL.ide
index 26c192baa..c4da84048 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -22,7 +22,7 @@ Else, read the rest of this document to compile your own CoqIde.
 
 COMPILATION REQUIREMENTS
 
-- OCaml >= 4.02.1 with native threads support.
+- OCaml >= 4.02.3 with native threads support.
 - make world must succeed.
 - The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
   The official supported version is at least 2.24.x.
diff --git a/configure.ml b/configure.ml
index 9d959b9af..b5d5a2419 100644
--- a/configure.ml
+++ b/configure.ml
@@ -601,14 +601,14 @@ let caml_version_nums =
          "Is it installed properly?")
 
 let check_caml_version () =
-  if caml_version_nums >= [4;2;1] then
+  if caml_version_nums >= [4;2;3] then
     cprintf "You have OCaml %s. Good!" caml_version
   else
     let () = cprintf "Your version of OCaml is %s." caml_version in
     if !prefs.force_caml_version then
       warn "Your version of OCaml is outdated."
     else
-      die "You need OCaml 4.02.1 or later."
+      die "You need OCaml 4.02.3 or later."
 
 let _ = check_caml_version ()
 
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 9d2ebf0d4..b5dd8445d 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux.
 
 In Coq source folder:
 
-opam switch 4.02.1+fp
+opam switch 4.02.3+fp
 ./configure -local -debug
 make
 perf record -g bin/coqtop -compile file.v
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 135c24aed..8127d3df3 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -104,7 +104,6 @@ exclude_patterns = [
     'Thumbs.db',
     '.DS_Store',
     'introduction.rst',
-    'credits.rst',
     'README.rst',
     'README.template.rst'
 ]
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index a75659798..2562dec46 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,3 +1,8 @@
+.. include:: preamble.rst
+.. include:: replaces.rst
+
+.. _credits:
+
 -------------------------------------------
 Credits
 -------------------------------------------
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 136f9088b..f3ae49381 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -1,16 +1,31 @@
-.. _introduction:
-
 .. include:: preamble.rst
 .. include:: replaces.rst
 
 .. include:: introduction.rst
-.. include:: credits.rst
 
 ------------------
 Table of contents
 ------------------
 
 .. toctree::
+   :caption: Indexes
+
+   genindex
+   coq-cmdindex
+   coq-tacindex
+   coq-optindex
+   coq-exnindex
+
+.. No entries yet
+  * :index:`thmindex`
+
+.. toctree::
+   :caption: Preamble
+
+   self
+   credits
+
+.. toctree::
    :caption: The language
 
    language/gallina-specification-language
@@ -65,18 +80,6 @@ Table of contents
 
    zebibliography
 
-.. toctree::
-   :caption: Indexes
-	     
-   genindex
-   coq-cmdindex
-   coq-tacindex	      
-   coq-optindex	      
-   coq-exnindex	      
-   
-.. No entries yet
-  * :index:`thmindex`
-
 This material (the Coq Reference Manual) may be distributed only subject to the
 terms and conditions set forth in the Open Publication License, v1.0 or later
 (the latest version is presently available at
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 75ff72c4d..20e4069f4 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,3 +1,5 @@
+.. _introduction:
+
 ------------------------
 Introduction
 ------------------------
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2c046190f..7fe2421f9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
     let cl = EConstr.Unsafe.to_constr cl in
     try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
     with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in
+  let gl = pf_merge_uc ucst gl in
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++
@@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl =
   | Cast(t, DEFAULTcast, ty) -> t, (gl, ty)
   | _ -> c, pfe_type_of gl c in
   let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in
-  let gl = pf_merge_uc ucst gl in
   Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl
 
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c20e415b4..9d9b1b2e8 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -561,8 +561,8 @@ let filter_upat i0 f n u fpats =
   let na = Array.length u.up_a in
   if n < na then fpats else
   let np = match u.up_k with
-  | KpatConst when equal u.up_f f -> na
-  | KpatFixed when equal u.up_f f -> na 
+  | KpatConst when eq_constr_nounivs u.up_f f -> na
+  | KpatFixed when eq_constr_nounivs u.up_f f -> na
   | KpatEvar k when isEvar_k k f -> na
   | KpatLet when isLetIn f -> na
   | KpatLam when isLambda f -> na
@@ -582,8 +582,8 @@ let filter_upat_FO i0 f n u fpats =
   let np = nb_args u.up_FO in
   if n < np then fpats else
   let ok = match u.up_k with
-  | KpatConst -> equal u.up_f f 
-  | KpatFixed -> equal u.up_f f 
+  | KpatConst -> eq_constr_nounivs u.up_f f
+  | KpatFixed -> eq_constr_nounivs u.up_f f
   | KpatEvar k -> isEvar_k k f
   | KpatLet -> isLetIn f
   | KpatLam -> isLambda f
@@ -764,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false)
       let match_let f = match kind f with
       | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b
       | _ -> false in match_let
-    | KpatFixed -> equal u.up_f
-    | KpatConst -> equal u.up_f
+    | KpatFixed -> eq_constr_nounivs u.up_f
+    | KpatConst -> eq_constr_nounivs u.up_f
     | KpatLam -> fun c ->
        (match kind c with
        | Lambda _ -> unif_EQ env sigma u.up_f c
diff --git a/test-suite/ssr/rew_polyuniv.v b/test-suite/ssr/rew_polyuniv.v
new file mode 100644
index 000000000..e2bbbc9ec
--- /dev/null
+++ b/test-suite/ssr/rew_polyuniv.v
@@ -0,0 +1,90 @@
+From Coq Require Import Utf8 Setoid ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+(** Telescopes *)
+Inductive tele : Type :=
+  | TeleO : tele
+  | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+  match TT with
+  | TeleO => T
+  | TeleS b => ∀ x, tele_fun (b x) T
+  end.
+
+Notation "TT -t> A" :=
+  (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+  takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+     match a in tele_arg TT return (TT -t> T) → T with
+     | TargO => λ t : T, t
+     | TargS x a => λ f, rec a (f x)
+     end) TT a f.
+Arguments tele_app {!_ _} _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Coercion tele_app : tele_fun >-> Funclass.
+
+(** Inversion lemma for [tele_arg] *)
+Lemma tele_arg_inv {TT : tele} (a : TT) :
+  match TT as TT return TT → Prop with
+  | TeleO => λ a, a = TargO
+  | TeleS f => λ a, ∃ x a', a = TargS x a'
+  end a.
+Proof. induction a; eauto. Qed.
+Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
+Proof. exact (tele_arg_inv a). Qed.
+Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
+  ∃ x a', a = TargS x a'.
+Proof. exact (tele_arg_inv a). Qed.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+  match TT as TT return (TT → U) → TT -t> U with
+  | TeleO => λ F, F TargO
+  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+                  tele_bind (λ a, F (TargS x a))
+  end.
+Arguments tele_bind {_ !_} _ /.
+
+(* Show that tele_app ∘ tele_bind is the identity. *)
+Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
+  (tele_app (tele_bind f)) x = f x.
+Proof.
+  induction TT as [|X b IH]; simpl in *.
+  - rewrite (tele_arg_O_inv x). auto.
+  - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl.
+    rewrite IH. auto.
+Qed.
+
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
+   binder so that, after simplifying, this matches the way we typically write
+   notations involving telescopes. *)
+Notation "'λ..' x .. y , e" :=
+  (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
+  (at level 200, x binder, y binder, right associativity,
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e").
+
+(* The testcase *)
+Lemma test {TA TB : tele} {X} (α' β' γ' : X → Prop) (Φ : TA → TB → Prop) x' :
+  (forall P Q, ((P /\ Q) = Q) * ((P -> Q) = Q)) ->
+  ∀ a b, Φ a b = (λ.. x y, β' x' ∧ (γ' x' → Φ x y)) a b.
+Proof.
+intros cheat a b.
+rewrite !tele_app_bind.
+by rewrite !cheat.
+Qed.
diff --git a/test-suite/ssr/set_polyuniv.v b/test-suite/ssr/set_polyuniv.v
new file mode 100644
index 000000000..436eeafc7
--- /dev/null
+++ b/test-suite/ssr/set_polyuniv.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+Axiom foo : Type -> Prop.
+
+Lemma test : foo nat.
+Proof.
+set x := foo _. (* key @foo{i} matches @foo{j} *)
+Abort.