From cedcfc9bc386456f3fdd225f739706e4f7a2902c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 10:51:08 +0100
Subject: Refine tactic now shelves unifiable holes.

The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
---
 test-suite/bugs/closed/3685.v |  4 ++--
 test-suite/bugs/closed/3686.v |  4 ++--
 test-suite/bugs/closed/3699.v | 16 ++++++++--------
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3