Merge branch 'v8.5'

7 files changed, 99 insertions, 4 deletions

diff --git a/test-suite/bugs/closed/3735.v b/test-suite/bugs/closed/3735.v
new file mode 100644
index 000000000..a50572ace
--- /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/3807.v b/test-suite/bugs/closed/3807.v
new file mode 100644
index 000000000..108ebf592
--- /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/4284.v b/test-suite/bugs/closed/4284.v
new file mode 100644
index 000000000..0fff3026f
--- /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)).
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index 0623cf5b8..43c9b5129 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/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
new file mode 100644
index 000000000..5c23f8404
--- /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 000000000..9eeb86468
--- /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
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2371d32cd..b72a06740 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.