From 161e23caa72d632d6bc308669674f4d8e10e95e6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 Jan 2016 05:36:16 +0100
Subject: [PATCH] No need to 'Set Bullet Behavior' everywhere.

Since ssr ad273277 the Global Set Bullet Behavior in modures.base
should do the job.
---
 barrier/heap_lang.v | 4 +---
 iris/parameter.v    | 6 ++----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index f67a22da5..9dfcbf9cd 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,7 +1,5 @@
 Require Import Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language iris.parameter.
-
-Set Bullet Behavior "Strict Subproofs".
+Require Import prelude.option prelude.gmap iris.parameter.
 
 (** 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). *)
diff --git a/iris/parameter.v b/iris/parameter.v
index 66a71493c..cfbf73ee3 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -1,7 +1,5 @@
 Require Export modures.cmra iris.language.
 
-Set Bullet Behavior "Strict Subproofs".
-
 Record iParam := IParam {
   iexpr : Type;
   ival : Type;
@@ -29,6 +27,8 @@ Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
 Qed.
 
+Canonical Structure istateC Σ := leibnizC (istate Σ).
+
 Definition IParamConst {iexpr ival istate : Type}
            (ilanguage : Language iexpr ival istate)
            (icmra : cmraT) {icmra_empty : Empty icmra}
@@ -39,5 +39,3 @@ Unshelve.
 - by intros.
 - by intros.
 Defined.
-
-Canonical Structure istateC Σ := leibnizC (istate Σ).
-- 
GitLab