diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3685.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3686.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3699.v | 16 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 4 | ||||
| -rw-r--r-- | theories/Logic/Hurkens.v | 89 |
6 files changed, 60 insertions, 59 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 35efb0b657..ca65f08ec0 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -357,7 +357,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in - Tactics.New.refine ~unsafe:false update + Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable end TACTIC EXTEND refine 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/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index cdc3e04610..18faacbaf6 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 4e582934af..5c87011e5c 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. |