From 88aa11081a72f1ef5ed99b144b4447779ccfa77c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 6 Nov 2019 20:19:23 +0100 Subject: [PATCH] More sensible instance names for `monPred`'s `BiAffine` and `BiPositive`. --- theories/bi/monpred.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v index dbb10db82..95394a06b 100644 --- a/theories/bi/monpred.v +++ b/theories/bi/monpred.v @@ -435,9 +435,9 @@ Proof. unseal. split. solve_proper. Qed. Global Instance monPred_in_flip_mono : Proper ((⊑) ==> flip (⊢)) (@monPred_in I PROP). Proof. solve_proper. Qed. -Global Instance monPred_positive : BiPositive PROP → BiPositive monPredI. +Global Instance monPred_bi_positive : BiPositive PROP → BiPositive monPredI. Proof. split => ?. unseal. apply bi_positive. Qed. -Global Instance monPred_affine : BiAffine PROP → BiAffine monPredI. +Global Instance monPred_bi_affine : BiAffine PROP → BiAffine monPredI. Proof. split => ?. unseal. by apply affine. Qed. Global Instance monPred_at_persistent P i : Persistent P → Persistent (P i). -- GitLab