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.

2 files changed, 47 insertions, 46 deletions

diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index cdc3e0461..18faacbaf 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -442,10 +442,10 @@ Section Proof_irrelevance_WEM_CC.
   Theorem wproof_irrelevance_cc : ~~(b1 = b2).
   Proof.
     intros h.
-    refine (let NB := exist (fun P=>~~P -> P) B _ in _).
+    unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)).
     { exact (fun _ => b1). }
     pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox.
-    refine (let F := exist (fun P=>~~P->P) False _ in _).
+    unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)).
     { auto. }
     exact (paradox F).
   Qed.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 4e582934a..5c87011e5 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -266,7 +266,7 @@ End Paradox.
 
 (** The [paradox] tactic can be called as a shortcut to use the paradox. *)
 Ltac paradox h :=
-  refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1.
+  unshelve (refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ))).
 
 End Generic.
 
@@ -319,25 +319,26 @@ Proof.
   + cbn. exact (fun u F => forall x:u, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
+
   + cbn. exact (fun F => u22u1 (forall x, F x)).
   + cbn. exact (fun _ x => u22u1_unit _ x).
   + cbn. exact (fun _ x => u22u1_counit _ x).
-  + cbn. intros **. now rewrite u22u1_coherent.
   (** Small universe *)
   + exact U0.
   (** The interpretation of the small universe is the image of
       [U0] in [U1]. *)
   + cbn. exact (fun X => u02u1 X).
   + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))).
-  + cbn. intros * x. exact (u12u0_unit _ x).
-  + cbn. intros * x. exact (u12u0_counit _ x).
   + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))).
-  + cbn. intros * x. exact (u12u0_unit _ x).
-  + cbn. intros * x. exact (u12u0_counit _ x).
   + cbn. exact (u12u0 F).
   + cbn in h.
     exact (u12u0_counit _ h).
+  + cbn. easy.
+  + cbn. intros **. now rewrite u22u1_coherent.
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
 Qed.
 
 End Paradox.
@@ -381,7 +382,7 @@ Qed.
 
 Definition Forall {A:Type} (P:A->MProp) : MProp.
 Proof.
-  refine (exist _ _ _).
+  unshelve (refine (exist _ _ _)).
   + exact (forall x:A, El (P x)).
   + intros h x.
     eapply strength in h.
@@ -411,27 +412,27 @@ Proof.
   + exact (fun _ => Forall).
   + cbn. exact (fun _ _ f => f).
   + cbn. exact (fun _ _ f => f).
-  + cbn. easy.
   + exact Forall.
   + cbn. exact (fun _ f => f).
   + cbn. exact (fun _ f => f).
-  + cbn. easy.
   (** Small universe *)
   + exact bool.
   + exact (fun b => El (b2p b)).
   + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + apply p2b.
+    exact B.
+  + cbn in h. auto.
+  + cbn. easy.
+  + cbn. easy.
   + cbn. auto.
   + cbn. intros * f.
     apply p2p1 in f. cbn in f.
     exact f.
-  + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
   + cbn. auto.
   + cbn. intros * f.
     apply p2p1 in f. cbn in f.
     exact f.
-  + apply p2b.
-    exact B.
-  + cbn in h. auto.
 Qed.
 
 End Paradox.
@@ -469,18 +470,18 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem paradox : forall B:NProp, El B.
 Proof.
   intros B.
-  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
   + exact (fun P => ~~P).
-  + cbn. auto.
-  + cbn. auto.
-  + cbn. auto.
   + exact bool.
   + exact p2b.
   + exact b2p.
-  + auto.
-  + auto.
   + exact B.
   + exact h.
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + auto.
+  + auto.
 Qed.
 
 End Paradox.
@@ -515,18 +516,18 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem mparadox : forall B:NProp, El B.
 Proof.
   intros B.
-  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
   + exact (fun P => P).
-  + cbn. auto.
-  + cbn. auto.
-  + cbn. auto.
   + exact bool.
   + exact p2b.
   + exact b2p.
-  + auto.
-  + auto.
   + exact B.
   + exact h.
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + auto.
+  + auto.
 Qed.
 
 End MParadox.
@@ -548,8 +549,8 @@ Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
 Theorem paradox : forall B:Prop, B.
 Proof.
   intros B.
-  refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
-                   (exist _ B (fun x => x))).
+  unshelve (refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+                   (exist _ B (fun x => x)))).
   + intros p. red. red. exact (p2b (El p)).
   + cbn. intros b. red. exists (b2p b). exact (fun x => x).
   + cbn. intros [A H]. cbn. apply p2p1.
@@ -596,7 +597,6 @@ Proof.
   + cbn. exact (fun u F => forall x, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
   + exact (fun F => forall A:Prop, F(up A)).
   + cbn. exact (fun F f A => f (up A)).
   + cbn.
@@ -604,20 +604,21 @@ Proof.
     specialize (f (down A)).
     rewrite up_down in f.
     exact f.
+  + exact Prop.
+  + cbn. exact (fun X => X).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact P.
+  + exact h.
+  + cbn. easy.
   + cbn.
     intros F f A.
     destruct (up_down A). cbn.
     reflexivity.
-  + exact Prop.
-  + cbn. exact (fun X => X).
-  + cbn. exact (fun A P => forall x:A, P x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. exact (fun A P => forall x:A, P x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. exact P.
-  + exact h.
 Qed.
 
 End Paradox.
@@ -664,37 +665,37 @@ Proof.
   + cbn. exact (fun X F => forall x:X, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
   + exact (fun F => forall x:A, F (up x)).
   + cbn. exact (fun _ f => fun x:A => f (up x)).
   + cbn. intros * f X.
     specialize (f (down X)).
     rewrite up_down in f.
     exact f.
-  + cbn. intros ? f X.
-    destruct (up_down X). cbn.
-    reflexivity.
   (** Small universe *)
   + exact A.
   (** The interpretation of [A] as a universe is [U]. *)
   + cbn. exact up.
   + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. exact (down False).
+  + rewrite up_down in p.
+    exact p.
+  + cbn. easy.
+  + cbn. intros ? f X.
+    destruct (up_down X). cbn.
+    reflexivity.
   + cbn. intros ? ? f.
     rewrite up_down.
     exact f.
   + cbn. intros ? ? f.
     rewrite up_down in f.
     exact f.
-  + cbn. exact (fun _ F => down (forall x, up (F x))).
   + cbn. intros ? ? f.
     rewrite up_down.
     exact f.
   + cbn. intros ? ? f.
     rewrite up_down in f.
     exact f.
-  + cbn. exact (down False).
-  + rewrite up_down in p.
-    exact p.
 Qed.
 
 End Paradox.
@@ -710,7 +711,7 @@ Module PropNeqType.
 Theorem paradox : Prop <> Type.
 Proof.
   intros h.
-  refine (TypeNeqSmallType.paradox _ _).
+  unshelve (refine (TypeNeqSmallType.paradox _ _)).
   + exact Prop.
   + easy.
 Qed.