Commit 75ed8394 authored by Ralf Jung's avatar Ralf Jung
Browse files

update for Coq 8.10 deprecations

parent 195f8e9e
...@@ -2,12 +2,9 @@ ...@@ -2,12 +2,9 @@
# We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there # We sometimes want to locally override notation (e.g. in proofmode/base.v, bi/embedding.v), and there
# is no good way to do that with scopes. # is no good way to do that with scopes.
-arg -w -arg -notation-overridden -arg -w -arg -notation-overridden
# Non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9. # Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294)
-arg -w -arg -redundant-canonical-projection -arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
theories/algebra/monoid.v theories/algebra/monoid.v
theories/algebra/cmra.v theories/algebra/cmra.v
......
...@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva ...@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
From iris.bi Require Import ascii. From iris.bi Require Import ascii.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *) Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section base_logic_tests. Section base_logic_tests.
Context {M : ucmraT}. Context {M : ucmraT}.
......
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *) Unset Printing Use Implicit Types. (* FIXME: remove once we drop support for Coq <=8.11. *)
Section tests. Section tests.
Context {I : biIndex} {PROP : bi}. Context {I : biIndex} {PROP : bi}.
......
...@@ -794,6 +794,7 @@ Record rFunctor := RFunctor { ...@@ -794,6 +794,7 @@ Record rFunctor := RFunctor {
Existing Instances rFunctor_map_ne rFunctor_mor. Existing Instances rFunctor_map_ne rFunctor_mor.
Instance: Params (@rFunctor_map) 9 := {}. Instance: Params (@rFunctor_map) 9 := {}.
Declare Scope rFunctor_scope.
Delimit Scope rFunctor_scope with RF. Delimit Scope rFunctor_scope with RF.
Bind Scope rFunctor_scope with rFunctor. Bind Scope rFunctor_scope with rFunctor.
...@@ -866,6 +867,7 @@ Record urFunctor := URFunctor { ...@@ -866,6 +867,7 @@ Record urFunctor := URFunctor {
Existing Instances urFunctor_map_ne urFunctor_mor. Existing Instances urFunctor_map_ne urFunctor_mor.
Instance: Params (@urFunctor_map) 9 := {}. Instance: Params (@urFunctor_map) 9 := {}.
Declare Scope urFunctor_scope.
Delimit Scope urFunctor_scope with URF. Delimit Scope urFunctor_scope with URF.
Bind Scope urFunctor_scope with urFunctor. Bind Scope urFunctor_scope with urFunctor.
......
...@@ -704,6 +704,7 @@ Record oFunctor := OFunctor { ...@@ -704,6 +704,7 @@ Record oFunctor := OFunctor {
Existing Instance oFunctor_map_ne. Existing Instance oFunctor_map_ne.
Instance: Params (@oFunctor_map) 9 := {}. Instance: Params (@oFunctor_map) 9 := {}.
Declare Scope oFunctor_scope.
Delimit Scope oFunctor_scope with OF. Delimit Scope oFunctor_scope with OF.
Bind Scope oFunctor_scope with oFunctor. Bind Scope oFunctor_scope with oFunctor.
......
...@@ -26,6 +26,7 @@ Record monPred := ...@@ -26,6 +26,7 @@ Record monPred :=
monPred_mono : Proper (() ==> ()) monPred_at }. monPred_mono : Proper (() ==> ()) monPred_at }.
Local Existing Instance monPred_mono. Local Existing Instance monPred_mono.
Declare Scope monPred.
Bind Scope monPred with bi. Bind Scope monPred with bi.
Implicit Types P Q : monPred. Implicit Types P Q : monPred.
......
...@@ -179,4 +179,5 @@ Reserved Notation "'[∗' 'mset]' x ∈ X , P" ...@@ -179,4 +179,5 @@ Reserved Notation "'[∗' 'mset]' x ∈ X , P"
format "[∗ mset] x ∈ X , P"). format "[∗ mset] x ∈ X , P").
(** Define the scope *) (** Define the scope *)
Declare Scope bi_scope.
Delimit Scope bi_scope with I. Delimit Scope bi_scope with I.
...@@ -2,9 +2,6 @@ From iris.program_logic Require Import language. ...@@ -2,9 +2,6 @@ From iris.program_logic Require Import language.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
(** Coercions to make programs easier to type. *) (** Coercions to make programs easier to type. *)
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
......
...@@ -27,9 +27,13 @@ Structure language := Language { ...@@ -27,9 +27,13 @@ Structure language := Language {
prim_step : expr state list observation expr state list expr Prop; prim_step : expr state list observation expr state list expr Prop;
language_mixin : LanguageMixin of_val to_val prim_step language_mixin : LanguageMixin of_val to_val prim_step
}. }.
Declare Scope expr_scope.
Delimit Scope expr_scope with E. Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr. Bind Scope expr_scope with expr.
Declare Scope val_scope.
Delimit Scope val_scope with V.
Bind Scope val_scope with val. Bind Scope val_scope with val.
Arguments Language {_ _ _ _ _ _ _} _. Arguments Language {_ _ _ _ _ _ _} _.
......
...@@ -234,7 +234,7 @@ an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q ...@@ -234,7 +234,7 @@ an efficient way. Concretely, we made sure that [envs_entails (Envs Γp Γs c) Q
and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This and [envs_entails (Envs Γp Γs c') Q] are convertible for any [c] and [c']. This
way, [iFresh] can simply be implemented by changing the goal from way, [iFresh] can simply be implemented by changing the goal from
[envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q] [envs_entails (Envs Γp Γs c) Q] into [envs_entails (Envs Γp Γs (Pos_succ c)) Q]
using the tactic [convert_concl_no_check]. This way, the generated proof term using the tactic [change_no_check]. This way, the generated proof term
contains no additional steps for changing the counter. contains no additional steps for changing the counter.
For all definitions below, we first define a version that take the two contexts For all definitions below, we first define a version that take the two contexts
......
...@@ -123,7 +123,7 @@ Ltac iFresh := ...@@ -123,7 +123,7 @@ Ltac iFresh :=
lazymatch goal with lazymatch goal with
| |- envs_entails (Envs ?Δp ?Δs _) ?Q => | |- envs_entails (Envs ?Δp ?Δs _) ?Q =>
let c' := eval vm_compute in (Pos.succ c) in let c' := eval vm_compute in (Pos.succ c) in
convert_concl_no_check (envs_entails (Envs Δp Δs c') Q) change_no_check (envs_entails (Envs Δp Δs c') Q)
end in end in
constr:(IAnon c). constr:(IAnon c).
......
...@@ -2,6 +2,7 @@ From stdpp Require Export strings. ...@@ -2,6 +2,7 @@ From stdpp Require Export strings.
From iris.proofmode Require Import coq_tactics environments. From iris.proofmode Require Import coq_tactics environments.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Declare Scope proof_scope.
Delimit Scope proof_scope with env. Delimit Scope proof_scope with env.
Arguments Envs _ _%proof_scope _%proof_scope _. Arguments Envs _ _%proof_scope _%proof_scope _.
Arguments Enil {_}. Arguments Enil {_}.
......
...@@ -22,9 +22,9 @@ Declare Reduction pm_eval := cbv [ ...@@ -22,9 +22,9 @@ Declare Reduction pm_eval := cbv [
Ltac pm_eval t := Ltac pm_eval t :=
eval pm_eval in t. eval pm_eval in t.
Ltac pm_reduce := Ltac pm_reduce :=
(* Use [convert_concl_no_check] instead of [change] to avoid performing the (* Use [change_no_check] instead of [change] to avoid performing the
conversion check twice. *) conversion check twice. *)
match goal with |- ?u => let v := pm_eval u in convert_concl_no_check v end. match goal with |- ?u => let v := pm_eval u in change_no_check v end.
Ltac pm_reflexivity := pm_reduce; exact eq_refl. Ltac pm_reflexivity := pm_reduce; exact eq_refl.
(** Called by many tactics for redexes that are created by instantiation. (** Called by many tactics for redexes that are created by instantiation.
...@@ -38,6 +38,6 @@ Declare Reduction pm_prettify := cbn [ ...@@ -38,6 +38,6 @@ Declare Reduction pm_prettify := cbn [
bi_tforall bi_texist bi_tforall bi_texist
]. ].
Ltac pm_prettify := Ltac pm_prettify :=
(* Use [convert_concl_no_check] instead of [change] to avoid performing the (* Use [change_no_check] instead of [change] to avoid performing the
conversion check twice. *) conversion check twice. *)
match goal with |- ?u => let v := eval pm_prettify in u in convert_concl_no_check v end. match goal with |- ?u => let v := eval pm_prettify in u in change_no_check v end.
...@@ -10,6 +10,8 @@ Record siProp := SiProp { ...@@ -10,6 +10,8 @@ Record siProp := SiProp {
}. }.
Arguments siProp_holds : simpl never. Arguments siProp_holds : simpl never.
Add Printing Constructor siProp. Add Printing Constructor siProp.
Declare Scope siProp_scope.
Delimit Scope siProp_scope with SI. Delimit Scope siProp_scope with SI.
Bind Scope siProp_scope with siProp. Bind Scope siProp_scope with siProp.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment