Merge branch 'v8.5'

7 files changed, 18 insertions, 18 deletions

diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
index a5bea34a98..7a0c3e6f1d 100644
--- a/test-suite/bugs/closed/3685.v
+++ b/test-suite/bugs/closed/3685.v
@@ -39,11 +39,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v
index b650920b26..df5f667480 100644
--- a/test-suite/bugs/closed/3686.v
+++ b/test-suite/bugs/closed/3686.v
@@ -33,11 +33,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 62137f0c06..aad0bb44d5 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +47,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +111,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +124,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/closed/3923.v
index 6aa6b4932e..0aa029e73d 100644
--- a/test-suite/bugs/opened/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -30,4 +30,4 @@ Axiom empty_fieldstore : cert_fieldstore.
 
 End MkCertRuntimeTypes.
 
-Fail Extraction MkCertRuntimeTypes.
+Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
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.