Merge branch 'ralf/less-coerce' into 'master'

only locally make uPred_holds a coercion

See merge request iris/iris!631

iris/base_logic/algebra.v

@@ -4,6 +4,7 @@ From iris.base_logic Require Import bi derived.
 From iris.prelude Require Import options.
 
 (** Internalized properties of our CMRA constructions. *)
+Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section upred.
 Context {M : ucmra}.

iris/base_logic/bi.v

@@ -240,7 +240,7 @@ End restate.
 
 
 (** New unseal tactic that also unfolds the BI layer.
-    This is used by [base_logic.bupd_alt].
+    This is used by [base_logic.algebra] and [base_logic.bupd_alt].
     TODO: Can we get rid of this? *)
 Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
   unfold bi_emp; simpl;

iris/base_logic/bupd_alt.v

@@ -25,6 +25,8 @@ We show that:
 
 The first two points are shown for any BI with a plain modality. *)
 
+Local Coercion uPred_holds : uPred >-> Funclass.
+
 Section bupd_alt.
   Context `{BiPlainly PROP}.
   Implicit Types P Q R : PROP.

iris/base_logic/upred.v

@@ -105,11 +105,15 @@ This completes the proof.
 *)
 
 Record uPred (M : ucmra) : Type := UPred {
-  uPred_holds :> nat → M → Prop;
+  uPred_holds : nat → M → Prop;
 
   uPred_mono n1 n2 x1 x2 :
     uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ≤ n1 → uPred_holds n2 x2
 }.
+(** When working in the model, it is convenient to be able to treat [uPred] as
+[nat → M → Prop].  But we only want to locally break the [uPred] abstraction
+this way. *)
+Local Coercion uPred_holds : uPred >-> Funclass.
 Bind Scope bi_scope with uPred.
 Global Arguments uPred_holds {_} _%I _ _ : simpl never.
 Add Printing Constructor uPred.

iris/si_logic/siprop.v

@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
 define the usual connectives of higher-order logic, and prove that these satisfy
 the usual laws of higher-order logic. *)
 Record siProp := SiProp {
-  siProp_holds :> nat → Prop;
+  siProp_holds : nat → Prop;
   siProp_closed n1 n2 : siProp_holds n1 → n2 ≤ n1 → siProp_holds n2
 }.
+Local Coercion siProp_holds : siProp >-> Funclass.
 Global Arguments siProp_holds : simpl never.
 Add Printing Constructor siProp.