4 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
index f808cb45e9..5932c9c56e 100644
--- a/test-suite/bugs/closed/4116.v
+++ b/test-suite/bugs/closed/4116.v
@@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
   Trunc_is_trunc : IsTrunc_internal n A.
 
 Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
-  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _);
   [
       | (
         let H := match goal with H := _ |- _ => constr:(H) end in
@@ -321,7 +321,7 @@ Section Grothendieck.
 
   Definition Gcategory : PreCategory.
   Proof.
-    refine (@Build_PreCategory
+    unshelve refine (@Build_PreCategory
               Pair
               (fun s d => Gmorphism s d)
               Gidentity
@@ -346,7 +346,7 @@ Section Grothendieck2.
   Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
   Proof.
     intros s d.
-    refine (isequiv_adjointify _ _ _ _).
+    unshelve refine (isequiv_adjointify _ _ _ _).
     {
       intro m.
       transparent assert (H' : (s.(c) = d.(c))).
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
index e86b3be64e..ea3347a851 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/931.v
@@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop.
 
 Goal Prop.
   refine (P _ _).
-  2:instantiate (1:=0).
+    instantiate (1:=0).
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
index 5fa167038d..d77b9b63a2 100644
--- a/test-suite/bugs/closed/HoTT_coq_090.v
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
 Instance isequiv_path {A B : Type} (p : A = B)
   : IsEquiv (transport (fun X:Type => X) p) | 0.
 Proof.
-  refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
+  unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
   admit.
 Defined.
 
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 1e667884b8..352abb2af5 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -62,7 +62,7 @@ Abort.
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 intro P.
  refine (P _ _).
-2:reflexivity.
+reflexivity.
 Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)