Merge branch 'simon/proofmode_primitive_projections' into 'master'

Add more primitive projections

See merge request iris/iris!873

iris/bi/embedding.v

@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op.
 From iris.bi Require Import plainly updates internal_eq.
 From iris.prelude Require Import options.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with [Type*]. *)
 Set Default Proof Using "Type*".
 

iris/bi/interface.v

 From iris.algebra Require Export ofe.
 From iris.bi Require Export notation.
 From iris.prelude Require Import options.
-Set Primitive Projections.
+
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
 
 Section bi_mixin.
   Context {PROP : Type} `{!Dist PROP, !Equiv PROP}.

iris/bi/internal_eq.v

@@ -2,6 +2,11 @@ From iris.bi Require Import derived_laws_later big_op.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (** This file defines a type class for BIs with a notion of internal equality.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_

iris/bi/plainly.v

@@ -3,6 +3,11 @@ From iris.bi Require Import derived_laws_later big_op internal_eq.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add [BiAffine] and the like, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 

iris/bi/updates.v

@@ -3,6 +3,11 @@ From iris.bi Require Import interface derived_laws_later big_op plainly.
 From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
+(* We enable primitive projections in this file to improve the performance of the Iris proofmode:
+    primitive projections for the bi-records makes the proofmode faster.
+*)
+Local Set Primitive Projections.
+
 (* The sections add extra BI assumptions, which is only picked up with "Type"*. *)
 Set Default Proof Using "Type*".
 

tests/heap_lang.ref

@@ -174,7 +174,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   ============================
   @bi_emp_valid (uPredI (iResUR Σ))
     (@fupd (bi_car (uPredI (iResUR Σ)))
-       (@bi_fupd_fupd (uPredI (iResUR Σ))
+       (@bi_fupd_fupd _
           (@uPred_bi_fupd HasLc Σ
              (@iris_invGS HasLc heap_lang Σ (@heapGS_irisGS HasLc Σ heapGS0))))
        (@top coPset coPset_top) (@top coPset coPset_top)