Merge branch 'v8.5'

5 files changed, 153 insertions, 0 deletions

diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fac3..f9154ef576 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 957612ef1d..d6bbfe29ac 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 :=. 
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 61e73f8587..c83f45e2a4 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 0000000000..db2bbb0dc7
--- /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/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 0000000000..31d264f645
--- /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.
+
+
+Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file