15 files changed, 367 insertions, 19 deletions

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index cc8cec47..f934a5c7 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -62,3 +62,47 @@ Axiom cast_coalesce :
   ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
 
 Hint Rewrite cast_coalesce : ltamer.
+
+Require Import Program.
+Module HintCut.
+Class A (f : nat -> nat) := a : True.
+Class B (f : nat -> nat) := b : True.
+Class C (f : nat -> nat) := c : True.
+Class D (f : nat -> nat) := d : True.
+Class E (f : nat -> nat) := e : True.
+
+Instance a_is_b f : A f -> B f.
+Proof. easy. Qed.
+Instance b_is_c f : B f -> C f.
+Proof. easy. Qed.
+Instance c_is_d f : C f -> D f.
+Proof. easy. Qed.
+Instance d_is_e f : D f -> E f.
+Proof. easy. Qed.
+
+Instance a_compose f g : A f -> A g -> A (compose f g).
+Proof. easy. Qed.
+Instance b_compose f g : B f -> B g -> B (compose f g).
+Proof. easy. Qed.
+Instance c_compose f g : C f -> C g -> C (compose f g).
+Proof. easy. Qed.
+Instance d_compose f g : D f -> D g -> D (compose f g).
+Proof. easy. Qed.
+Instance e_compose f g : E f -> E g -> E (compose f g).
+Proof. easy. Qed.
+
+Instance a_id : A id.
+Proof. easy. Qed.
+
+Instance foo f :
+  E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘
+     id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id).
+Proof.
+  Fail Timeout 1 apply _. (* 3.7s *)
+  
+Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ;
+  (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
+
+  Timeout 1 Fail apply _. (* 0.06s *)
+Abort.
+End HintCut.
\ No newline at end of file
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a4ed76c5..55b666b7 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -333,13 +333,10 @@ exact (refl_equal 3).
 exact (refl_equal 4).
 Qed.
 
-(* From 12612, descent in conjunctions is more powerful *)
+(* From 12612, Dec 2009, descent in conjunctions is more powerful *)
 (* The following, which was failing badly in bug 1980, is now
    properly rejected, as descend in conjunctions builds an
-   ill-formed elimination from Prop to Type.
-
-   Added Aug 2014: why it fails is now that trivial unification ?x = goal is
-   rejected by the descent in conjunctions to avoid surprising results. *)
+   ill-formed elimination from Prop to the domain of ex which is in Type. *)
 
 Goal True.
 Fail eapply ex_intro.
@@ -351,28 +348,32 @@ Fail eapply (ex_intro _).
 exact I.
 Qed.
 
-(* Note: the following succeed directly (i.e. w/o "exact I") since
-   Aug 2014 since the descent in conjunction does not use a "cut"
-   anymore: the iota-redex is contracted and we get rid of the
-   uninstantiated evars
-
-   Is it good or not? Maybe it does not matter so much.
+(* No failure here, because the domain of ex is in Prop *)
 
 Goal True.
-eapply (ex_intro (fun _ => True) I).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I).
+reflexivity.
 Qed.
 
 Goal True.
-eapply (ex_intro (fun _ => True) I _).    
-exact I. (* Not needed since Aug 2014 *)
+eapply (ex_intro (fun _ => 0=0) I _).
+Unshelve. (* In 8.4:  Grab Existential Variables. *)
+reflexivity.
 Qed.
 
 Goal True.
 eapply (fun (A:Prop) (x:A) => conj I x).
-exact I. (* Not needed since Aug 2014 *)
+Unshelve. (* In 8.4: the goal ?A was there *)
+exact I.
 Qed.
-*)
+
+(* Testing compatibility mode with v8.4 *)
+
+Goal True.
+Fail eapply existT.
+Set Universal Lemma Under Conjunction.
+eapply existT.
+Abort.
 
 (* The following was not accepted from r12612 to r12657 *)
 
@@ -463,6 +464,7 @@ Abort.
 Goal forall H:0=0, H = H.
 intros.
 Fail apply eq_sym in H.
+Abort.
 
 (* Check that unresolved evars not originally present in goal prevent
    apply in to work*)
@@ -546,3 +548,14 @@ apply (foo ?y).
 Grab Existential Variables.
 exact 0.
 Qed.
+
+(* Test position of new hypotheses when using "apply ... in ... as ..." *)
+Goal (True -> 0=0 /\ True) -> True -> False -> True/\0=0.
+intros H H0 H1.
+apply H in H0 as (a,b).
+(* clear H1:False *) match goal with H:_ |- _ => clear H end.
+split.
+- (* use b:True *) match goal with H:_ |- _ => exact H end.
+- (* clear b:True *) match goal with H:_ |- _ => clear H end.
+  (* use a:0=0 *) match goal with H:_ |- _ => exact H end.
+Qed.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index db3b19af..aaa7b3a5 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -1,6 +1,6 @@
 (* Wish #2154 by E. van der Weegen *)
 
-(* auto was not using f_equal-style lemmas with metavariables occuring
+(* auto was not using f_equal-style lemmas with metavariables occurring
    only in the type of an evar of the concl, but not directly in the
    concl itself *)
 
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
new file mode 100644
index 00000000..7215bd99
--- /dev/null
+++ b/test-suite/success/extraction_polyprop.v
@@ -0,0 +1,11 @@
+(* The current extraction cannot handle this situation,
+   and shouldn't try, otherwise it might produce some Ocaml
+   code that segfaults. See Table.error_singleton_become_prop
+   or S. Glondu's thesis for more details. *)
+
+Definition f {X} (p : (nat -> X) * True) : X * nat :=
+  (fst p 0, 0).
+
+Definition f_prop := f ((fun _ => I),I).
+
+Fail Extraction f_prop.
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 9443d01e..35ba94fb 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -33,3 +33,39 @@ Goal True -> True -> True.
 intros _ ?.
 exact H.
 Qed.
+
+(* A short test about introduction pattern pat/c *)
+Goal (True -> 0=0) -> True /\ False -> 0=0.
+intros H (H1/H,_).
+exact H1.
+Qed.
+
+(* A test about bugs in 8.5beta2 *)
+Goal (True -> 0=0) -> True /\ False -> False -> 0=0.
+intros H H0 H1.
+destruct H0 as (a/H,_).
+(* Check that H0 is removed (was bugged in 8.5beta2) *)
+Fail clear H0.
+(* Check position of newly created hypotheses when using pat/c (was
+   left at top in 8.5beta2) *)
+match goal with H:_ |- _ => clear H end. (* clear H1:False *)
+match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *)
+Qed.
+
+Goal (True -> 0=0) -> True -> 0=0.
+intros H H1/H.
+exact H1.
+Qed.
+
+Goal forall n, n = S n -> 0=0.
+intros n H/n_Sn.
+destruct H.
+Qed.
+
+(* Another check about generated names and cleared hypotheses with
+   pat/c patterns *)
+Goal (True -> 0=0 /\ 1=1) -> True -> 0=0.
+intros H (H1,?)/H.
+change (1=1) in H0.
+exact H1.
+Qed.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index badce063..6c4d4ae9 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -298,3 +298,22 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check instantiation of binders using ltac names *)
+
+Goal True.
+let x := ipattern:y in assert (forall x y, x = y + 0).
+intro.
+destruct y. (* Check that the name is y here *)
+Abort.
+
+(* An example suggested by Jason (see #4317) showing the intended semantics *)
+(* Order of binders is reverted because y is just told to depend on x *)
+
+Goal 1=1.
+let T := constr:(fun a b : nat => a) in
+  lazymatch T with
+  | (fun x z => ?y) => pose ((fun x x => y) 2 1)
+  end.
+exact (eq_refl n).
+Qed.
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fa..f9154ef5 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -4,6 +4,8 @@
 (* Fail  exact H. *)
 (* Section . *)
 
+Unset Strict Universe Declaration.
+
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9167c9fc..d6bbfe29 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,5 @@
+Unset Strict Universe Declaration.
+
 Module withoutpoly.
 
 Inductive empty :=. 
@@ -292,3 +294,31 @@ Section foo2.
   Context `{forall A B, Funext A B}.
   Print Universes.
 End foo2.
+
+Module eta.
+Set Universe Polymorphism.
+
+Set Printing Universes.
+
+Axiom admit : forall A, A.
+Record R := {O : Type}.
+
+Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
+Definition RLRL' : forall x : R, RL x = RL (RL x).
+  intros. apply eq_refl.
+Qed.
+
+End eta.
+
+Module Hurkens'.
+  Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
+Type)) eq_refl.
+
+End Hurkens'.
\ No newline at end of file
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 068f8ac3..125615c5 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -188,3 +188,10 @@ Set Printing All.
 Check (@p' nat).
 Check p'.
 Unset Printing All.
+
+Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
+
+Definition term (x : wrap nat) := x.(unwrap).
+Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
+Recursive Extraction term term'.
+(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f85..c83f45e2 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -117,5 +117,81 @@ End T1.
 
 Check (bla 7 : 2 = 8).
 
+Section A.
+Variable a : nat.
+Variable b : nat.
+Variable c : nat.
+Variable H1 : a = 3.
+Variable H2 : a = 3 -> b = 7.
+Variable H3 : c = 3.
+
+Lemma foo : a = a.
+Proof using Type*.
+pose H1 as e1.
+pose H2 as e2.
+reflexivity.
+Qed.
+
+Lemma bar : a = 3 -> b = 7.
+Proof using b*.
+exact H2.
+Qed.
+
+Lemma baz : c=3.
+Proof using c*.
+exact H3.
+Qed.
+
+Lemma baz2 : c=3.
+Proof using c* a.
+exact H3.
+Qed.
+
+End A.
+
+Check (foo 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (bar 3 7 (refl_equal 3)
+               (fun _ => refl_equal 7)).
+Check (baz2 99 3 (refl_equal 3)).
+Check (baz 3 (refl_equal 3)).
+
+Section Let.
+
+Variables a b : nat.
+Let pa : a = a. Proof. reflexivity. Qed.
+Unset Default Proof Using.
+Set Suggest Proof Using.
+Lemma test_let : a = a.
+Proof using a.
+exact pa.
+Qed.
+
+Let ppa : pa = pa. Proof. reflexivity. Qed.
+
+Lemma test_let2 : pa = pa.
+Proof using Type.
+exact ppa.
+Qed.
+
+End Let.
+
+Check (test_let 3).
+
+Section Clear.
+
+Variable a: nat.
+Hypotheses H : a = 4.
+
+Set Proof Using Clear Unused.
+
+Lemma test_clear : a = a.
+Proof using a.
+Fail rewrite H.
+trivial.
+Qed.
+
+End Clear.
+
 
 
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
new file mode 100644
index 00000000..db2bbb0d
--- /dev/null
+++ b/test-suite/success/record_syntax.v
@@ -0,0 +1,47 @@
+Module A.
+
+Record Foo := { foo : unit; bar : unit }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt
+|}.
+
+Definition foo0 (p : Foo) := match p with {| |} => tt end.
+Definition foo1 (p : Foo) := match p with {| foo := f |} => f end.
+Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end.
+Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end.
+Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end.
+
+End A.
+
+Module B.
+
+Record Foo := { }.
+
+End B.
+
+Module C.
+
+Record Foo := { foo : unit; bar : unit; }.
+
+Definition foo_ := {|
+  foo := tt;
+  bar := tt;
+|}.
+
+End C.
+
+Module D.
+
+Record Foo := { foo : unit }.
+Definition foo_ := {| foo := tt |}.
+
+End D.
+
+Module E.
+
+Record Foo := { foo : unit; }.
+Definition foo_ := {| foo := tt; |}.
+
+End E.
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
new file mode 100644
index 00000000..3c0b8156
--- /dev/null
+++ b/test-suite/success/sideff.v
@@ -0,0 +1,12 @@
+Definition idw (A : Type) := A.
+Lemma foobar : unit.
+Proof.
+  Require Import Program.
+  apply (const tt tt).
+Qed.
+
+Lemma foobar' : unit.
+  Lemma aux : forall A : Type, A -> unit.
+  Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
+  apply (@aux unit tt).
+Qed.
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index e540ae5f..5b87e877 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *)
 simpl (unbox _ (unbox _ _)) at 2 4.
 match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end.
 Abort.
+
+(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *)
+
+Goal 2=1+1.
+match goal with |- (_ = ?c) => simpl c end.
+match goal with |- 2 = 2 => idtac end. (* Check that it reduced *)
+Abort.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index c5f032be..3faa1ca4 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -45,4 +45,22 @@ specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)
 
-Abort.
\ No newline at end of file
+Abort.
+
+(* Test use of pose proof and assert as a specialize *)
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+pose proof (H I) as H.
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.
+
+Goal True -> (True -> 0=0) -> False -> 0=0.
+intros H0 H H1.
+assert (H:=H I).
+(* Check that the hypothesis is in 2nd position by removing the top one *)
+match goal with H:_ |- _ => clear H end.
+match goal with H:_ |- _ => exact H end.
+Qed.
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 00000000..048b53d2
--- /dev/null
+++ b/test-suite/success/univnames.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
+
+Set Printing Universes.
+
+Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
+
+Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
+
+Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
+
+Definition nothing (A : Type) := A.
+
+Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
+
+Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
+
+
+Monomorphic Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file