Skip to content
Snippets Groups Projects
Commit 0ecd47dc authored by Simon Spies's avatar Simon Spies Committed by Ralf Jung
Browse files

Use primitive projections for all BI records

parent 2a4c815d
No related branches found
No related tags found
No related merge requests found
......@@ -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*".
......
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}.
......
......@@ -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_
......
......@@ -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*".
......
......@@ -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*".
......
......@@ -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)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment