From 566a24e28924ad4a7dda99891dce3882e6db112c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Nov 2015 16:01:33 +0100
Subject: Adding the Printing Projections options to the index.

---
 doc/refman/RefMan-ext.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d21c91201d..b77118e1f9 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -253,6 +253,7 @@ Reset Initial.
 
 \Rem An experimental syntax for projections based on a dot notation is
 available. The command to activate it is
+\optindex{Printing Projections}
 \begin{quote}
 {\tt Set Printing Projections.}
 \end{quote}
-- 
cgit v1.2.3


From 11ccb7333c2a82d59736027838acaea2237e2402 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 26 Nov 2015 18:09:53 +0100
Subject: Make the pretty printer resilient to incomplete nametab (progress on
 #4363).

The nametab in which the error message is printed is not the one in
which the error message happens.

This reveals a weakness in the fix_exn code: the fix_exn function should
be pure, while in some cases (like this one) uses the global state (the
nametab) to print a term in a pretty way (the shortest non-ambiguous name
for constants).

This patch makes the externalization phase (used by term printing)
resilient to an incomplete nametab, so that printing a term in the
wrong nametab does not mask the original error.
---
 interp/constrextern.ml | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb0..5160f07af0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l)
     For instance, in the debugger the tables of global references
     may be inaccurate *)
 
+let safe_shortest_qualid_of_global vars r =
+  try shortest_qualid_of_global vars r
+  with Not_found ->
+    match r with
+    | VarRef v -> make_qualid DirPath.empty v
+    | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c))
+    | IndRef (i,_) | ConstructRef ((i,_),_) ->
+        make_qualid DirPath.empty Names.(Label.to_id (mind_label i))
+
 let default_extern_reference loc vars r =
-  Qualid (loc,shortest_qualid_of_global vars r)
+  Qualid (loc,safe_shortest_qualid_of_global vars r)
 
 let my_extern_reference = ref default_extern_reference
 
-- 
cgit v1.2.3


From 982460743a54ecfab1d601ba930d61c04972d17a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Nov 2015 19:05:25 +0100
Subject: Fixing the "parsing rules with idents later declared as keywords"
 problem.

The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
---
 parsing/tok.ml                 | 1 +
 test-suite/success/Notations.v | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/parsing/tok.ml b/parsing/tok.ml
index efd57968d2..12140f4036 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -21,6 +21,7 @@ type t =
   | EOI
 
 let equal t1 t2 = match t1, t2 with
+| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
 | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
 | METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
 | PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2371d32cda..b72a067407 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end.
 
 Parameter traverse : (nat -> unit) -> (nat -> unit).
 Notation traverse_var f l := (traverse (fun l => f l) l).
+
+(* Check that when an ident become a keyword, it does not break
+   previous rules relying on the string to be classified as an ident *)
+
+Notation "'intros' x" := (S x) (at level 0).
+Goal True -> True. intros H. exact H. Qed.
-- 
cgit v1.2.3


From 8297baa98147f78263126b1bd6cf41b0456f177d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2015 17:21:10 +0100
Subject: Fix [Polymorphic Hint Rewrite].

---
 tactics/extratactics.ml4  | 2 +-
 toplevel/vernacentries.ml | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cab74968d2..9ffcd2dcff 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -264,7 +264,7 @@ TACTIC EXTEND rewrite_star
 let add_rewrite_hint bases ort t lcsr =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let poly = Flags.is_universe_polymorphism () in 
+  let poly = Flags.use_polymorphic_flag () in
   let f ce = 
     let c, ctx = Constrintern.interp_constr env sigma ce in
     let ctx =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 177c3fb0ab..2b23323248 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2048,7 +2048,7 @@ let check_vernac_supports_polymorphism c p =
 
 let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
-  | Some b -> b
+  | Some b -> Flags.make_polymorphic_flag b; b
 
 (** A global default timeout, controled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
@@ -2149,7 +2149,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             then Flags.verbosely (interp ?proof ~loc locality poly) c
             else Flags.silently  (interp ?proof ~loc locality poly) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
-            Flags.program_mode := orig_program_mode
+            Flags.program_mode := orig_program_mode;
+	  ignore (Flags.use_polymorphic_flag ())
           end
         with
         | reraise when
@@ -2161,6 +2162,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
             let e = locate_if_not_already loc e in
             let () = restore_timeout () in
             Flags.program_mode := orig_program_mode;
+	    ignore (Flags.use_polymorphic_flag ());
             iraise e
   and aux_list ?locality ?polymorphism isprogcmd l =
     List.iter (aux false) (List.map snd l)
-- 
cgit v1.2.3


From a0e72610a71e086da392c8563c2eec2e35211afa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2015 17:21:35 +0100
Subject: Avoid recording spurious Set <= Top.i constraints which are always
 valid (when Top.i is global and hence > Set).

---
 library/universes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/universes.ml b/library/universes.ml
index 6cccb10efb..1b6f7a9d57 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -854,7 +854,7 @@ let normalize_context_set ctx us algs =
     Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) ->
         if d == Le then
 	  if Univ.Level.is_small l then
-	    if is_set_minimization () then
+	    if is_set_minimization () && LSet.mem r ctx then
 	      (Constraint.add cstr smallles, noneqs)
 	    else (smallles, noneqs)
 	  else if Level.is_small r then
-- 
cgit v1.2.3


From 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 27 Nov 2015 20:34:51 +0100
Subject: Univs: entirely disallow instantiation of polymorphic constants with
 Prop levels.

As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
---
 kernel/univ.ml                  |   6 +-
 library/declare.ml              |   2 +-
 library/universes.ml            |   2 +-
 pretyping/pretyping.ml          |  30 ++++++----
 test-suite/bugs/closed/4287.v   |   6 +-
 theories/Classes/CMorphisms.v   |  14 +----
 theories/Logic/ClassicalFacts.v |   1 -
 theories/Logic/Hurkens.v        | 121 ++++++++++++++++++++++++----------------
 8 files changed, 102 insertions(+), 80 deletions(-)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index dc0a4b43c0..2b3a2bdb11 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1707,7 +1707,9 @@ struct
     else if Array.length y = 0 then x 
     else Array.append x y
 
-  let of_array a = a
+  let of_array a =
+    assert(Array.for_all (fun x -> not (Level.is_prop x)) a);
+    a
 
   let to_array a = a
 
@@ -1715,7 +1717,7 @@ struct
 
   let subst_fn fn t = 
     let t' = CArray.smartmap fn t in
-      if t' == t then t else t'
+      if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x
 
diff --git a/library/declare.ml b/library/declare.ml
index 5968fbf38b..994a6557ad 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -431,7 +431,7 @@ let cache_universes (p, l) =
 		     Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
   in
-    Global.push_context_set false ctx;
+    Global.push_context_set p ctx;
     if p then Lib.add_section_context ctx;
     Universes.set_global_universe_names glob'
 
diff --git a/library/universes.ml b/library/universes.ml
index 1b6f7a9d57..a8e9478e13 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
-	      else 
+	      else
 		try let lev = Option.get (Universe.level inst) in
 		      Constraint.add (lev, d, r) cstrs
 		with Option.IsNone -> failwith "")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index dd4fcf1981..faba5c7563 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -394,18 +394,22 @@ let pretype_global loc rigid env evd gr us =
     match us with
     | None -> evd, None
     | Some l -> 
-      let _, ctx = Universes.unsafe_constr_of_global gr in
-      let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
-      let len = Array.length arr in
-	if len != List.length l then
-	  user_err_loc (loc, "pretype", 
-			str "Universe instance should have length " ++ int len)
-	else
-	  let evd, l' = List.fold_left (fun (evd, univs) l -> 
+       let _, ctx = Universes.unsafe_constr_of_global gr in
+       let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
+       let len = Array.length arr in
+       if len != List.length l then
+	 user_err_loc (loc, "pretype", 
+		       str "Universe instance should have length " ++ int len)
+       else
+	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
 	    let evd, l = interp_universe_level_name evd l in
 	      (evd, l :: univs)) (evd, []) l
-      in 
-	evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
+	 in
+	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
+	   user_err_loc (loc, "pretype",
+		 str "Universe instances cannot contain Prop, polymorphic" ++
+		   str " universe instances must be greater or equal to Set.");
+	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
   in
     Evd.fresh_global ~rigid ?names:instance env evd gr
 
@@ -440,13 +444,15 @@ let pretype_sort evdref = function
 
 let new_type_evar env evdref loc =
   let e, s = 
-    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
+    evd_comb0 (fun evd -> Evarutil.new_type_evar env evd
+      univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
   in e
 
 let get_projection env cst =
   let cb = lookup_constant cst env in
     match cb.Declarations.const_proj with
-    | Some {Declarations.proj_ind = mind; proj_npars = n; proj_arg = m; proj_type = ty} -> 
+    | Some {Declarations.proj_ind = mind; proj_npars = n;
+	    proj_arg = m; proj_type = ty} -> 
       (cst,mind,n,m,ty)
     | None -> raise Not_found
 
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b84..43c9b51295 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) :=
   let foo (A : Type@{j}) := A in foo B.
 
 Fail Check @setlt@{j Prop}.
-Check @setlt@{Prop j}.
-Check @setle@{Prop j}.
-
 Fail Definition foo := @setle@{j Prop}.
-Definition foo := @setle@{Prop j}.
+Check setlt@{Set i}.
+Check setlt@{Set j}.
\ No newline at end of file
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index fdedbf672a..b13671cec0 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -269,16 +269,6 @@ Section GenericInstances.
   Unset Strict Universe Declaration.
   
   (** The complement of a crelation conserves its proper elements. *)
-  Program Definition complement_proper (A : Type@{k}) (RA : crelation A)
-          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-    Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _.
-  
-  Next Obligation.
-  Proof.
-    unfold complement.
-    pose (mR x y X x0 y0 X0).
-    intuition.
-  Qed.
  
   (** The [flip] too, actually the [flip] instance is a bit more general. *)
   Program Definition flip_proper
@@ -521,8 +511,8 @@ Ltac proper_reflexive :=
 Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
 Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
-Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
-  : typeclass_instances.
+(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper  *)
+(*   : typeclass_instances. *)
 Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
   : typeclass_instances.
 Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 6f736e45fd..cdc3e04610 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -658,4 +658,3 @@ Proof.
     exists x; intro; exact Hx.
     exists x0; exact Hnot.
 Qed.
-
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index ede51f57f9..4e582934af 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -344,53 +344,6 @@ End Paradox.
 
 End NoRetractToImpredicativeUniverse.
 
-(** * Prop is not a retract *)
-
-(** The existence in the pure Calculus of Constructions of a retract
-    from [Prop] into a small type of [Prop] is inconsistent. This is a
-    special case of the previous result. *)
-
-Module NoRetractFromSmallPropositionToProp.
-
-Section Paradox.
-
-(** ** Retract of [Prop] in a small type *)
-
-(** The retract is axiomatized using logical equivalence as the
-    equality on propositions. *)
-
-Variable bool : Prop.
-Variable p2b : Prop -> bool.
-Variable b2p : bool -> Prop.
-Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
-Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
-
-(** ** Paradox *)
-
-Theorem paradox : forall B:Prop, B.
-Proof.
-  intros B.
-  pose proof
-      (NoRetractToImpredicativeUniverse.paradox@{Type Prop}) as P.
-  refine (P _ _ _ _ _ _ _ _ _ _);clear P.
-  + exact bool.
-  + exact (fun x => forall P:Prop, (x->P)->P).
-  + cbn. exact (fun _ x P k => k x).
-  + cbn. intros F P x.
-    apply P.
-    intros f.
-    exact (f x).
-  + cbn. easy.
-  + exact b2p.
-  + exact p2b.
-  + exact p2p2.
-  + exact p2p1.
-Qed.
-
-End Paradox.
-
-End NoRetractFromSmallPropositionToProp.
-
 (** * Modal fragments of [Prop] are not retracts *)
 
 (** In presence of a a monadic modality on [Prop], we can define a
@@ -534,6 +487,80 @@ End Paradox.
 
 End NoRetractToNegativeProp.
 
+(** * Prop is not a retract *)
+
+(** The existence in the pure Calculus of Constructions of a retract
+    from [Prop] into a small type of [Prop] is inconsistent. This is a
+    special case of the previous result. *)
+
+Module NoRetractFromSmallPropositionToProp.
+
+(** ** The universe of propositions. *)
+
+Definition NProp := { P:Prop | P -> P}.
+Definition El : NProp -> Prop := @proj1_sig _ _.
+
+Section MParadox.
+
+(** ** Retract of [Prop] in a small type, using the identity modality. *)
+
+Variable bool : NProp.
+Variable p2b : NProp -> El bool.
+Variable b2p : El bool -> NProp.
+Hypothesis p2p1 : forall A:NProp, El (b2p (p2b A)) -> El A.
+Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
+
+(** ** Paradox *)
+
+Theorem mparadox : forall B:NProp, El B.
+Proof.
+  intros B.
+  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  + exact (fun P => P).
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + exact bool.
+  + exact p2b.
+  + exact b2p.
+  + auto.
+  + auto.
+  + exact B.
+  + exact h.
+Qed.
+
+End MParadox.
+
+Section Paradox.
+
+(** ** Retract of [Prop] in a small type *)
+
+(** The retract is axiomatized using logical equivalence as the
+    equality on propositions. *)
+Variable bool : Prop.
+Variable p2b : Prop -> bool.
+Variable b2p : bool -> Prop.
+Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
+Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
+
+(** ** Paradox *)
+
+Theorem paradox : forall B:Prop, B.
+Proof.
+  intros B.
+  refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+                   (exist _ B (fun x => x))).
+  + intros p. red. red. exact (p2b (El p)).
+  + cbn. intros b. red. exists (b2p b). exact (fun x => x).
+  + cbn. intros [A H]. cbn. apply p2p1.
+  + cbn. intros [A H]. cbn. apply p2p2.
+Qed.
+
+End Paradox.
+
+End NoRetractFromSmallPropositionToProp.
+
+
 (** * Large universes are no retracts of [Prop]. *)
 
 (** The existence in the Calculus of Constructions with universes of a
-- 
cgit v1.2.3


From 90fef3ffd236f2ed5575b0d11a47185185abc75b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 28 Nov 2015 19:41:17 +0100
Subject: Univs: correctly register universe binders for lemmas.

---
 proofs/pfedit.ml        | 10 +++++---
 proofs/pfedit.mli       |  7 +++++-
 proofs/proof_global.ml  | 28 +++++++++++++++-------
 proofs/proof_global.mli | 17 +++++++------
 stm/lemmas.ml           | 63 ++++++++++++++++++++++++++-----------------------
 stm/lemmas.mli          | 15 +++++++-----
 toplevel/command.ml     |  6 +++--
 7 files changed, 88 insertions(+), 58 deletions(-)

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 02dbd1fdcb..cbccf00e72 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name
 let get_all_proof_names = Proof_global.get_all_proof_names
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
 
 let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
+let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof sigma id str goals terminator;
+  Proof_global.start_proof sigma id ?pl str goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -54,6 +55,9 @@ let set_used_variables l =
 let get_used_variables () =
   Proof_global.get_used_variables ()
 
+let get_universe_binders () =
+  Proof_global.get_universe_binders ()
+
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
   | NoSuchGoal -> Errors.error "No such goal."
@@ -139,7 +143,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
-    const, status, univs
+    const, status, fst univs
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fc521ea432..d0528c9fdf 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -55,8 +55,10 @@ val delete_all_proofs : unit -> unit
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 
+type universe_binders = Id.t Loc.located list
+
 val start_proof :
-  Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -121,6 +123,9 @@ val set_used_variables :
   Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> universe_binders option
+
 (** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c303f486c5..3d60ff217a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -63,14 +63,14 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
@@ -89,6 +89,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode Ephemeron.key;
+  universe_binders: universe_binders option;
 }
 
 (* The head of [!pstates] is the actual current proof, the other ones are
@@ -226,7 +227,7 @@ let disactivate_proof_mode mode =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints). *)
-let start_proof sigma id str goals terminator =
+let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -234,10 +235,11 @@ let start_proof sigma id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
-let start_dependent_proof id str goals terminator =
+let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -245,10 +247,12 @@ let start_dependent_proof id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
+let get_universe_binders () = (cur_pstate ()).universe_binders
 
 let proof_using_auto_clear = ref true
 let _ = Goptions.declare_bool_option
@@ -296,7 +300,8 @@ let get_open_goals () =
     List.length shelf
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
-  let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+    cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
@@ -362,8 +367,13 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
 	  const_entry_polymorphic = poly})
-      fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength; universes = universes },
+		fpl initial_goals in
+  let binders =
+    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
+	       universe_binders
+  in
+  { id = pid; entries = entries; persistence = strength;
+    universes = (universes, binders) },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a22545080b..ea7fc7cfa8 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -55,18 +55,18 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Names.Id.t Loc.located list
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
-  (** guards : lemma_possible_guards; *)
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
+		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -80,14 +80,15 @@ type closed_proof = proof_object * proof_terminator
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
-    proof_terminator -> unit
+  Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+  Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
@@ -140,6 +141,8 @@ val set_used_variables :
   Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+val get_universe_binders : unit -> universe_binders option
+
 (**********************************************************)
 (*                                                        *)
 (*                            Proof modes                 *)
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6c18326882..5f4e4deb47 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -186,7 +186,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -205,6 +205,7 @@ let save ?export_seff id const cstrs do_guard (locality,poly,kind) hook =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
           (locality, ConstRef kn) in
     definition_message id;
+    Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
   with e when Errors.noncritical e ->
     let e = Errors.push e in
@@ -219,11 +220,11 @@ let compute_proof_name locality = function
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
         user_err_loc (loc,"",pr_id id ++ str " already exists.");
-      id
+      id, pl
   | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -276,28 +277,28 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs do_guard persistence hook
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  save ?export_seff id const cstrs pl do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
-
 let save_anonymous ?export_seff proof save_ident =
-  let id,const,cstrs,do_guard,persistence,hook = proof in
+  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs do_guard persistence hook
+  save ?export_seff save_ident const cstrs pl do_guard persistence hook
 
 let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,cstrs,do_guard,_,hook = proof in
+  let id,const,(cstrs,pl),do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+  save ?export_seff save_ident const cstrs pl do_guard
+      (Global, const.const_entry_polymorphic, Proof kind) hook
 
 (* Admitted *)
 
-let admit (id,k,e) hook () =
+let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -306,6 +307,7 @@ let admit (id,k,e) hook () =
       str "declared as an axiom.")
   in
   let () = assumption_message id in
+  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -315,11 +317,10 @@ let set_start_hook = (:=) start_hook
 
 
 let get_proof proof do_guard hook opacity =
-  let (id,(const,cstrs,persistence)) =
+  let (id,(const,univs,persistence)) =
     Pfedit.cook_this_proof proof
   in
-  (** FIXME *)
-  id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
+  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
 
 let check_exist =
   List.iter (fun (loc,id) ->
@@ -329,16 +330,16 @@ let check_exist =
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe,ctx) ->
-      admit (id,k,pe) (hook (Some ctx)) ();
+  | Admitted (id,k,pe,(ctx,pl)) ->
+      admit (id,k,pe) pl (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
         | Vernacexpr.Transparent -> false, true, []
         | Vernacexpr.Opaque None -> true, false, []
         | Vernacexpr.Opaque (Some l) -> true, true, l in
-      let proof = get_proof proof compute_guard 
-	(hook (Some proof.Proof_global.universes)) is_opaque in
+      let proof = get_proof proof compute_guard
+	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some ((_,id),None) -> save_anonymous ~export_seff proof id
@@ -350,7 +351,7 @@ let universe_proof_terminator compute_guard hook =
 let standard_proof_terminator compute_guard hook =
   universe_proof_terminator compute_guard (fun _ -> hook)
 
-let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = standard_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -358,9 +359,9 @@ let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
-let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+let start_proof_univs id ?pl kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
   let terminator = universe_proof_terminator compute_guard hook in
   let sign = 
     match sign with
@@ -368,11 +369,11 @@ let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+  Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -380,7 +381,7 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with 
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+    in match List.map2 (fun ((id,_),(t,_)) n -> (id,n,t)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
@@ -409,7 +410,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
       (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start")
-  | (id,(t,(_,imps)))::other_thms ->
+  | ((id,pl),(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
         | None -> Evd.empty_evar_universe_context
@@ -428,7 +429,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook =
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
 	  call_hook (fun exn -> exn) hook strength ref) thms_data in
-      start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+      start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
 
 let start_proof_com kind thms hook =
   let env0 = Global.env () in
@@ -472,14 +473,13 @@ let save_proof ?proof = function
             if const_entry_type = None then
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
-            let ctx = Evd.evar_context_universe_context universes in
+            let ctx = Evd.evar_context_universe_context (fst universes) in
             Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
             let id, k, typ = Pfedit.current_proof_statement () in
             (* This will warn if the proof is complete *)
             let pproofs, universes =
               Proof_global.return_proof ~allow_partial:true () in
-            let ctx = Evd.evar_context_universe_context universes in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
@@ -489,7 +489,10 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
+	    let names = Pfedit.get_universe_binders () in
+            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
+		     (universes, Some binders))
       in
       Proof_global.get_terminator() pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 6556aa2297..376374cb85 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -14,7 +14,6 @@ open Vernacexpr
 open Pfedit
 
 type 'a declaration_hook
-
 val mk_hook :
   (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
 
@@ -24,20 +23,24 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
+val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
+val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
+  ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-  (Proof_global.proof_universes option -> unit declaration_hook) -> unit
+  (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-  goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
+  goal_kind -> Evd.evar_map ->
+  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t * universe_binders option) *
+     (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 val standard_proof_terminator :
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b709a3fc4..91cfddb547 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1128,7 +1128,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
@@ -1164,7 +1165,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in
+      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
         fixdefs) in
-- 
cgit v1.2.3


From 15aeb84a0deb444af81f4035dbcf791566bafe5f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 28 Nov 2015 19:43:58 +0100
Subject: Closed bugs.

---
 test-suite/bugs/closed/3807.v | 33 +++++++++++++++++++++++++++++++++
 test-suite/bugs/closed/4400.v | 19 +++++++++++++++++++
 test-suite/bugs/closed/4433.v | 29 +++++++++++++++++++++++++++++
 3 files changed, 81 insertions(+)
 create mode 100644 test-suite/bugs/closed/3807.v
 create mode 100644 test-suite/bugs/closed/4400.v
 create mode 100644 test-suite/bugs/closed/4433.v

diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v
new file mode 100644
index 0000000000..108ebf592b
--- /dev/null
+++ b/test-suite/bugs/closed/3807.v
@@ -0,0 +1,33 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+Unset Universe Minimization ToSet.
+
+
+Definition foo : Type := nat.
+About foo.
+(* foo@{Top.1} : Type@{Top.1}*)
+(* Top.1 |=  *)
+
+Definition bar : foo -> nat.
+Admitted.
+About bar.
+(* bar@{Top.2} : foo@{Top.2} -> nat *)
+(* Top.2 |=  *)
+
+Lemma baz@{i} : foo@{i} -> nat.
+Proof.
+  exact bar.
+Defined.
+
+Definition bar'@{i} : foo@{i} -> nat.
+  intros f. exact 0.
+Admitted.
+About bar'.
+(* bar'@{i} : foo@{i} -> nat *)
+(* i |=  *)
+
+Axiom f@{i} : Type@{i}.
+(*
+*** [ f@{i} : Type@{i} ]
+(* i |=  *)
+*)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
new file mode 100644
index 0000000000..5c23f8404b
--- /dev/null
+++ b/test-suite/bugs/closed/4400.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
+Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
+Set Printing Universes.
+Inductive Foo (I : Type -> Type) (A : Type) : Type :=
+| foo (B : Type) : A -> I B -> Foo I A.
+Definition Family := Type -> Type.
+Definition FooToo : Family -> Family := Foo.
+Definition optionize (I : Type -> Type) (A : Type) := option (I A).
+Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
+Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
+Definition barRec : Rec (optionize id) := {| rec := bar id |}.
+Inductive Empty {T} : T -> Prop := .
+Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
+nil)) (b : unit) :
+  Empty (a, b) -> False.
+Proof.
+  intro e.
+  dependent induction e.
+Qed.
diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v
new file mode 100644
index 0000000000..9eeb864689
--- /dev/null
+++ b/test-suite/bugs/closed/4433.v
@@ -0,0 +1,29 @@
+Require Import Coq.Arith.Arith Coq.Init.Wf.
+Axiom proof_admitted : False.
+Goal exists x y z : nat, Fix
+                           Wf_nat.lt_wf
+                           (fun _ => nat -> nat)
+                           (fun x' f => match x' as x'0
+                                              return match x'0 with
+                                                       | 0 => True
+                                                       | S x'' => x'' < x'
+                                                     end
+                                                     -> nat -> nat
+                                        with
+                                          | 0 => fun _ _ => 0
+                                          | S x'' => f x''
+                                        end
+                                          (match x' with
+                                             | 0 => I
+                                             | S x'' => (Nat.lt_succ_diag_r _)
+                                           end))
+                           z
+                           y
+                         = 0.
+Proof.
+  do 3 (eexists; [ shelve.. | ]).
+  match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end.
+  case proof_admitted.
+  Unshelve.
+  all:constructor.
+Defined.
\ No newline at end of file
-- 
cgit v1.2.3


From 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 28 Nov 2015 20:02:52 +0100
Subject: Test-suite files for closed bugs

---
 test-suite/bugs/closed/3735.v | 4 ++++
 test-suite/bugs/closed/4284.v | 6 ++++++
 2 files changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/3735.v
 create mode 100644 test-suite/bugs/closed/4284.v

diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v
new file mode 100644
index 0000000000..a50572ace0
--- /dev/null
+++ b/test-suite/bugs/closed/3735.v
@@ -0,0 +1,4 @@
+Require Import Coq.Program.Tactics.
+Class Foo := { bar : Type }.
+Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *)
+Fail Program Lemma foo : Foo -> bar. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v
new file mode 100644
index 0000000000..0fff3026ff
--- /dev/null
+++ b/test-suite/bugs/closed/4284.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
+Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True.
+Proof.
+set (Q1 := total2 (fun f => pr1 P f = x)).
+set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)).
-- 
cgit v1.2.3