Merge branch 'v8.5'

2 files changed, 11 insertions, 2 deletions

diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 35ba94fb6..741f372ff 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -69,3 +69,12 @@ intros H (H1,?)/H.
 change (1=1) in H0.
 exact H1.
 Qed.
+
+(* Checking iterated pat/c1.../cn introduction patterns and side conditions *)
+
+Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D.
+intros * H H0 H1.
+intros H2/H/H0.
+- exact H2.
+- exact H1.
+Qed.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index d6bbfe29a..878875bd9 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -242,7 +242,7 @@ Fail Check (Prop : Set).
 Fail Check (Set : Set).
 Check (Set : Type).
 Check (Prop : Type).
-Definition setType := $(let t := type of Set in exact t)$.
+Definition setType := ltac:(let t := type of Set in exact t).
 
 Definition foo (A : Prop) := A.
 
@@ -303,7 +303,7 @@ 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 RL (x : R@{i}) : ltac:(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.