Skip to content
Snippets Groups Projects
Commit ea07fcbc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove spurious type annotations (there is a `Implicit Type` here).

parent 2e76d24c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/proofmode/class_instances_bi.v
+ 3
− 3
View file @ ea07fcbc
...@@ -10,11 +10,11 @@ Implicit Types P Q R : PROP. ...@@ -10,11 +10,11 @@ Implicit Types P Q R : PROP.
Implicit Types mP : option PROP. Implicit Types mP : option PROP.
(** AsEmpValid *) (** AsEmpValid *)
Global Instance as_emp_valid_emp_valid (P : PROP) : AsEmpValid0 (bi_emp_valid P) P | 0. Global Instance as_emp_valid_emp_valid P : AsEmpValid0 (bi_emp_valid P) P | 0.
Proof. by rewrite /AsEmpValid. Qed. Proof. by rewrite /AsEmpValid. Qed.
Global Instance as_emp_valid_entails (P Q : PROP) : AsEmpValid0 (P ⊢ Q) (P -∗ Q). Global Instance as_emp_valid_entails P Q : AsEmpValid0 (P ⊢ Q) (P -∗ Q).
Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed. Proof. split. apply bi.entails_wand. apply bi.wand_entails. Qed.
Global Instance as_emp_valid_equiv (P Q : PROP) : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q). Global Instance as_emp_valid_equiv P Q : AsEmpValid0 (P ≡ Q) (P ∗-∗ Q).
Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed. Proof. split. apply bi.equiv_wand_iff. apply bi.wand_iff_equiv. Qed.
Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) : Global Instance as_emp_valid_forall {A : Type} (φ : A → Prop) (P : A → PROP) :
......
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