Commit 161e23ca authored by Robbert Krebbers's avatar Robbert Krebbers

No need to 'Set Bullet Behavior' everywhere.

Since ssr ad273277 the Global Set Bullet Behavior in modures.base
should do the job.
parent 80f07870
Require Import Autosubst.Autosubst. Require Import Autosubst.Autosubst.
Require Import prelude.option prelude.gmap iris.language iris.parameter. Require Import prelude.option prelude.gmap iris.parameter.
Set Bullet Behavior "Strict Subproofs".
(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1. (** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
They all assume such an equality is the first thing on the "stack" (goal). *) They all assume such an equality is the first thing on the "stack" (goal). *)
......
Require Export modures.cmra iris.language. Require Export modures.cmra iris.language.
Set Bullet Behavior "Strict Subproofs".
Record iParam := IParam { Record iParam := IParam {
iexpr : Type; iexpr : Type;
ival : Type; ival : Type;
...@@ -29,6 +27,8 @@ Proof. ...@@ -29,6 +27,8 @@ Proof.
by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist. by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
Qed. Qed.
Canonical Structure istateC Σ := leibnizC (istate Σ).
Definition IParamConst {iexpr ival istate : Type} Definition IParamConst {iexpr ival istate : Type}
(ilanguage : Language iexpr ival istate) (ilanguage : Language iexpr ival istate)
(icmra : cmraT) {icmra_empty : Empty icmra} (icmra : cmraT) {icmra_empty : Empty icmra}
...@@ -39,5 +39,3 @@ Unshelve. ...@@ -39,5 +39,3 @@ Unshelve.
- by intros. - by intros.
- by intros. - by intros.
Defined. Defined.
Canonical Structure istateC Σ := leibnizC (istate Σ).
Markdown is supported
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