Commit b07b7deb authored by Ralf Jung's avatar Ralf Jung

no longer silence ambiguous coercion paths, and fix other warnings

parent 2ec13e91
......@@ -7,8 +7,6 @@
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/barrier/proof.v
theories/barrier/specification.v
......
......@@ -205,7 +205,7 @@ Section conditional_counter.
pau P Q γ_n f is_gc_loc f
end)%I.
Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv.
Local Hint Extern 0 (environments.envs_entails _ (counter_inv _ _)) => unfold counter_inv : core.
Definition is_counter (γ_n : gname) (ctr : val) :=
( (c : loc), ctr = #c N ## gcN gc_inv inv counterN (counter_inv γ_n c))%I.
......
......@@ -283,7 +283,7 @@ Section rdcss.
accepted_state (Q n) (proph_extract_winner vs) tid_ghost_winner ))
own γ_s (Cinr $ to_agree ()) done_state (Q n) l_descr tid_ghost_winner γ_t γ_a))%I.
Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv.
Local Hint Extern 0 (environments.envs_entails _ (descr_inv _ _ _ _ _ _ _ _ _ _)) => unfold descr_inv : core.
Definition pau P Q l_n l_m m1 n1 n2 :=
( P - AU << (m n : val), (gc_mapsto l_m m) rdcss_state l_n n >> @ (∖↑N)∖↑gcN,
......@@ -316,7 +316,7 @@ Section rdcss.
pau P Q l_n l_m m1 n1 n2 is_gc_loc l_m
end)%I.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _)) => unfold rdcss_inv.
Local Hint Extern 0 (environments.envs_entails _ (rdcss_inv _)) => unfold rdcss_inv : core.
Definition is_rdcss (l_n : loc) :=
(inv rdcssN (rdcss_inv l_n) gc_inv N ## gcN)%I.
......
......@@ -16,10 +16,10 @@ Section lang_rules.
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step.
Local Hint Resolve to_of_val.
Local Hint Constructors head_step : core.
Local Hint Resolve to_of_val : core.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
......
......@@ -242,9 +242,9 @@ Definition is_atomic (e : expr) : Prop :=
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| _ => False
end.
Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
Local Hint Resolve language.val_irreducible : core.
Local Hint Resolve to_of_val : core.
Local Hint Unfold language.irreducible : core.
Global Instance is_atomic_correct s e : is_atomic e Atomic s e.
Proof.
intros Ha; apply strongly_atomic_atomic, ectx_language_atomic.
......@@ -260,5 +260,5 @@ Ltac solve_atomic :=
apply is_atomic_correct; simpl; repeat split;
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 0 (Atomic _ _) => solve_atomic.
Hint Extern 0 (Atomic _ _) => solve_atomic : core.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
......@@ -336,9 +336,9 @@ Definition is_atomic (e : expr) : Prop :=
is_Some (to_val e3)
| _ => False
end.
Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
Local Hint Resolve language.val_irreducible : core.
Local Hint Resolve to_of_val : core.
Local Hint Unfold language.irreducible : core.
Global Instance is_atomic_correct s e : is_atomic e Atomic s e.
Proof.
intros Ha; apply strongly_atomic_atomic, ectx_language_atomic.
......@@ -354,5 +354,5 @@ Ltac solve_atomic :=
apply is_atomic_correct; simpl; repeat split;
rewrite ?to_of_val; eapply mk_is_Some; fast_done.
Hint Extern 0 (Atomic _ _) => solve_atomic.
Hint Extern 0 (Atomic _ _) => solve_atomic : core.
Hint Extern 0 (Atomic _ _) => solve_atomic : typeclass_instances.
......@@ -17,10 +17,10 @@ Section stlc_rules.
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Constructors head_step.
Local Hint Resolve to_of_val.
Local Hint Constructors head_step : core.
Local Hint Resolve to_of_val : core.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
......
......@@ -459,7 +459,7 @@ Lemma in_op_dom' (G G' : Gmon) y : ✓(G ⋅ G') →
y dom (gset loc) (Gmon_graph G') y dom (gset loc) (Gmon_graph (G G')).
Proof. rewrite comm; apply in_op_dom. Qed.
Local Hint Resolve cmra_valid_op_l cmra_valid_op_r in_op_dom in_op_dom'.
Local Hint Resolve cmra_valid_op_l cmra_valid_op_r in_op_dom in_op_dom' : core.
Lemma in_op_dom_alt (G G' : Gmon) y : (G G')
y dom (gset loc) G y dom (gset loc) (G G').
......@@ -468,14 +468,14 @@ Lemma in_op_dom_alt' (G G' : Gmon) y : ✓(G ⋅ G') →
y dom (gset loc) G' y dom (gset loc) (G G').
Proof. intros HGG; rewrite -?Gmon_graph_dom; eauto. Qed.
Local Hint Resolve in_op_dom_alt in_op_dom_alt'.
Local Hint Resolve in_op_dom_alt in_op_dom_alt' : core.
Local Hint Extern 1 => eapply get_left_conv + eapply get_left_conv' +
eapply get_right_conv + eapply get_right_conv'.
eapply get_right_conv + eapply get_right_conv' : core.
Local Hint Extern 1 (_ dom (gset loc) (Gmon_graph _)) =>
erewrite Gmon_graph_dom.
erewrite Gmon_graph_dom : core.
Local Hint Resolve path_start path_end.
Local Hint Resolve path_start path_end : core.
Lemma path_conv (G G' : Gmon) x y p :
(G G') maximal (Gmon_graph G) x dom (gset _) G
......@@ -538,7 +538,7 @@ Lemma in_dom_singleton (x : loc) (w : chlO) :
Proof. by rewrite dom_singleton elem_of_singleton. Qed.
Local Hint Resolve graph_op_path graph_op_path' in_dom_singleton.
Local Hint Resolve graph_op_path graph_op_path' in_dom_singleton : core.
Lemma maximal_op (G G' : Gmon) : (G G') maximal (Gmon_graph G)
maximal (Gmon_graph G') maximal (Gmon_graph (G G')).
......@@ -566,7 +566,7 @@ Proof.
Qed.
Local Hint Resolve maximal_op_singleton maximal_op get_left_singleton
get_right_singleton.
get_right_singleton : core.
Lemma maximally_marked_tree_both (G G' : Gmon) x xl xr :
((x [] (Some xl, Some xr)) (G G'))
......
Markdown is supported
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