diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 9b3c0b9fdebbb512a28a8cd89a4edfee89050027..e1ec26565180a8e2539d0a0d91edc330a0e518ab 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -202,9 +202,9 @@ Qed. Program Definition fixpoint_def `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f} : A := compl (fixpoint_chain f). -Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed. -Definition fixpoint {A AC AiH} f {Hf} := proj1_sig fixpoint_aux A AC AiH f Hf. -Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux. +Definition fixpoint_aux : seal (@fixpoint_def). by eexists. Qed. +Definition fixpoint {A AC AiH} f {Hf} := unseal fixpoint_aux A AC AiH f Hf. +Definition fixpoint_eq : @fixpoint = @fixpoint_def := seal_eq fixpoint_aux. Section fixpoint. Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}. diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v index b15ba0355e35f7999af0f38c93ff77809c049989..679db07daf2433af296e6fd92e04d7485510425a 100644 --- a/theories/base_logic/derived.v +++ b/theories/base_logic/derived.v @@ -33,6 +33,7 @@ Class TimelessP {M} (P : uPred M) := timelessP : â–· P ⊢ â—‡ P. Arguments timelessP {_} _ {_}. Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ â–¡ P. +Hint Mode PersistentP - ! : typeclass_instances. Arguments persistentP {_} _ {_}. Module uPred. diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v index 6485be49e97315b6448239ca7e849f13ab56481c..d6817d63375f38bf3a4a3a045c105ff29a9b70a7 100644 --- a/theories/base_logic/lib/fancy_updates.v +++ b/theories/base_logic/lib/fancy_updates.v @@ -11,9 +11,9 @@ Import uPred. Program Definition fupd_def `{invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ := (wsat ∗ ownE E1 ==∗ â—‡ (wsat ∗ ownE E2 ∗ P))%I. -Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed. -Definition fupd := proj1_sig fupd_aux. -Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux. +Definition fupd_aux : seal (@fupd_def). by eexists. Qed. +Definition fupd := unseal fupd_aux. +Definition fupd_eq : @fupd = @fupd_def := seal_eq fupd_aux. Arguments fupd {_ _} _ _ _%I. Instance: Params (@fupd) 4. diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v index 00aa890dfd6ff69ce53e841c58a65f0f21626e42..74aa939fc3857aa58dda5dc21ef9425d47f9c84b 100644 --- a/theories/base_logic/lib/gen_heap.v +++ b/theories/base_logic/lib/gen_heap.v @@ -34,9 +34,9 @@ Section definitions. Definition mapsto_def (l : L) (q : Qp) (v: V) : iProp Σ := own gen_heap_name (â—¯ {[ l := (q, to_agree (v : leibnizC V)) ]}). - Definition mapsto_aux : { x | x = @mapsto_def }. by eexists. Qed. - Definition mapsto := proj1_sig mapsto_aux. - Definition mapsto_eq : @mapsto = @mapsto_def := proj2_sig mapsto_aux. + Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed. + Definition mapsto := unseal mapsto_aux. + Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux. End definitions. Local Notation "l ↦{ q } v" := (mapsto l q v) diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v index 5d002b353e4726d01a61bcbeffdcd9e40b9b37ad..7ca2fc14458cef7cf150cb0a13f9d690c4119bd5 100644 --- a/theories/base_logic/lib/invariants.v +++ b/theories/base_logic/lib/invariants.v @@ -8,9 +8,9 @@ Import uPred. (** Derived forms and lemmas about them. *) Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ := (∃ i, ⌜i ∈ ↑N⌠∧ ownI i P)%I. -Definition inv_aux : { x | x = @inv_def }. by eexists. Qed. -Definition inv {Σ i} := proj1_sig inv_aux Σ i. -Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux. +Definition inv_aux : seal (@inv_def). by eexists. Qed. +Definition inv {Σ i} := unseal inv_aux Σ i. +Definition inv_eq : @inv = @inv_def := seal_eq inv_aux. Instance: Params (@inv) 3. Typeclasses Opaque inv. diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v index f9610bb371087348ccbce885eb82b22e882d0459..3f23ca2d399596035188c22185b687886fcd7e5e 100644 --- a/theories/base_logic/lib/namespaces.v +++ b/theories/base_logic/lib/namespaces.v @@ -11,14 +11,14 @@ Definition nroot : namespace := nil. Definition ndot_def `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. -Definition ndot_aux : { x | x = @ndot_def }. by eexists. Qed. -Definition ndot {A A_dec A_count}:= proj1_sig ndot_aux A A_dec A_count. -Definition ndot_eq : @ndot = @ndot_def := proj2_sig ndot_aux. +Definition ndot_aux : seal (@ndot_def). by eexists. Qed. +Definition ndot {A A_dec A_count}:= unseal ndot_aux A A_dec A_count. +Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux. Definition nclose_def (N : namespace) : coPset := coPset_suffixes (encode N). -Definition nclose_aux : { x | x = @nclose_def }. by eexists. Qed. -Instance nclose : UpClose namespace coPset := proj1_sig nclose_aux. -Definition nclose_eq : @nclose = @nclose_def := proj2_sig nclose_aux. +Definition nclose_aux : seal (@nclose_def). by eexists. Qed. +Instance nclose : UpClose namespace coPset := unseal nclose_aux. +Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux. Notation "N .@ x" := (ndot N x) (at level 19, left associativity, format "N .@ x") : C_scope. diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v index 70130e8260ea2f7ecaebad4ceb0be5054bbfee12..dfcca18ca7ece752d8f93e1439755e322fd8638d 100644 --- a/theories/base_logic/lib/own.v +++ b/theories/base_logic/lib/own.v @@ -54,9 +54,9 @@ Instance: Params (@iRes_singleton) 4. Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ := uPred_ownM (iRes_singleton γ a). -Definition own_aux : { x | x = @own_def }. by eexists. Qed. -Definition own {Σ A i} := proj1_sig own_aux Σ A i. -Definition own_eq : @own = @own_def := proj2_sig own_aux. +Definition own_aux : seal (@own_def). by eexists. Qed. +Definition own {Σ A i} := unseal own_aux Σ A i. +Definition own_eq : @own = @own_def := seal_eq own_aux. Instance: Params (@own) 4. Typeclasses Opaque own. @@ -104,7 +104,7 @@ Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed. Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 â‹… a2 â‹… a3). Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed. Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a. -Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed. +Proof. apply: uPred.always_entails_r. apply own_valid. Qed. Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a. Proof. by rewrite comm -own_valid_r. Qed. diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v index 0ad4f620874b077c0a7c18fbb94bf1640d08bcee..d145a96b0233923d31f46109a0bcba18cca94c54 100644 --- a/theories/base_logic/primitive.v +++ b/theories/base_logic/primitive.v @@ -9,26 +9,26 @@ Local Hint Extern 10 (_ ≤ _) => omega. Program Definition uPred_pure_def {M} (φ : Prop) : uPred M := {| uPred_holds n x := φ |}. Solve Obligations with done. -Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed. -Definition uPred_pure {M} := proj1_sig uPred_pure_aux M. +Definition uPred_pure_aux : seal (@uPred_pure_def). by eexists. Qed. +Definition uPred_pure {M} := unseal uPred_pure_aux M. Definition uPred_pure_eq : - @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux. + @uPred_pure = @uPred_pure_def := seal_eq uPred_pure_aux. Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True). Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∧ Q n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. -Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed. -Definition uPred_and {M} := proj1_sig uPred_and_aux M. -Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux. +Definition uPred_and_aux : seal (@uPred_and_def). by eexists. Qed. +Definition uPred_and {M} := unseal uPred_and_aux M. +Definition uPred_and_eq: @uPred_and = @uPred_and_def := seal_eq uPred_and_aux. Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := P n x ∨ Q n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. -Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed. -Definition uPred_or {M} := proj1_sig uPred_or_aux M. -Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux. +Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed. +Definition uPred_or {M} := unseal uPred_or_aux M. +Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux. Program Definition uPred_impl_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', @@ -39,33 +39,33 @@ Next Obligation. eapply HPQ; auto. exists (x2 â‹… x4); by rewrite assoc. Qed. Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed. -Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed. -Definition uPred_impl {M} := proj1_sig uPred_impl_aux M. +Definition uPred_impl_aux : seal (@uPred_impl_def). by eexists. Qed. +Definition uPred_impl {M} := unseal uPred_impl_aux M. Definition uPred_impl_eq : - @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux. + @uPred_impl = @uPred_impl_def := seal_eq uPred_impl_aux. Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∀ a, Ψ a n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. -Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed. -Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A. +Definition uPred_forall_aux : seal (@uPred_forall_def). by eexists. Qed. +Definition uPred_forall {M A} := unseal uPred_forall_aux M A. Definition uPred_forall_eq : - @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux. + @uPred_forall = @uPred_forall_def := seal_eq uPred_forall_aux. Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M := {| uPred_holds n x := ∃ a, Ψ a n x |}. Solve Obligations with naive_solver eauto 2 with uPred_def. -Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed. -Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A. -Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux. +Definition uPred_exist_aux : seal (@uPred_exist_def). by eexists. Qed. +Definition uPred_exist {M A} := unseal uPred_exist_aux M A. +Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := seal_eq uPred_exist_aux. Program Definition uPred_internal_eq_def {M} {A : ofeT} (a1 a2 : A) : uPred M := {| uPred_holds n x := a1 ≡{n}≡ a2 |}. Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)). -Definition uPred_internal_eq_aux : { x | x = @uPred_internal_eq_def }. by eexists. Qed. -Definition uPred_internal_eq {M A} := proj1_sig uPred_internal_eq_aux M A. +Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). by eexists. Qed. +Definition uPred_internal_eq {M A} := unseal uPred_internal_eq_aux M A. Definition uPred_internal_eq_eq: - @uPred_internal_eq = @uPred_internal_eq_def := proj2_sig uPred_internal_eq_aux. + @uPred_internal_eq = @uPred_internal_eq_def := seal_eq uPred_internal_eq_aux. Program Definition uPred_sep_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 â‹… x2 ∧ P n x1 ∧ Q n x2 |}. @@ -79,9 +79,9 @@ Next Obligation. exists x1, x2; cofe_subst; split_and!; eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r. Qed. -Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed. -Definition uPred_sep {M} := proj1_sig uPred_sep_aux M. -Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux. +Definition uPred_sep_aux : seal (@uPred_sep_def). by eexists. Qed. +Definition uPred_sep {M} := unseal uPred_sep_aux M. +Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := seal_eq uPred_sep_aux. Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M := {| uPred_holds n x := ∀ n' x', @@ -92,10 +92,10 @@ Next Obligation. eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le. Qed. Next Obligation. naive_solver. Qed. -Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed. -Definition uPred_wand {M} := proj1_sig uPred_wand_aux M. +Definition uPred_wand_aux : seal (@uPred_wand_def). by eexists. Qed. +Definition uPred_wand {M} := unseal uPred_wand_aux M. Definition uPred_wand_eq : - @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux. + @uPred_wand = @uPred_wand_def := seal_eq uPred_wand_aux. Program Definition uPred_always_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := P n (core x) |}. @@ -103,10 +103,10 @@ Next Obligation. intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN. Qed. Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed. -Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed. -Definition uPred_always {M} := proj1_sig uPred_always_aux M. +Definition uPred_always_aux : seal (@uPred_always_def). by eexists. Qed. +Definition uPred_always {M} := unseal uPred_always_aux M. Definition uPred_always_eq : - @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux. + @uPred_always = @uPred_always_def := seal_eq uPred_always_aux. Program Definition uPred_later_def {M} (P : uPred M) : uPred M := {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}. @@ -116,10 +116,10 @@ Qed. Next Obligation. intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia. Qed. -Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed. -Definition uPred_later {M} := proj1_sig uPred_later_aux M. +Definition uPred_later_aux : seal (@uPred_later_def). by eexists. Qed. +Definition uPred_later {M} := unseal uPred_later_aux M. Definition uPred_later_eq : - @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux. + @uPred_later = @uPred_later_def := seal_eq uPred_later_aux. Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M := {| uPred_holds n x := a ≼{n} x |}. @@ -128,18 +128,18 @@ Next Obligation. exists (a' â‹… x2). by rewrite (assoc op) Hx1. Qed. Next Obligation. naive_solver eauto using cmra_includedN_le. Qed. -Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed. -Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M. +Definition uPred_ownM_aux : seal (@uPred_ownM_def). by eexists. Qed. +Definition uPred_ownM {M} := unseal uPred_ownM_aux M. Definition uPred_ownM_eq : - @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux. + @uPred_ownM = @uPred_ownM_def := seal_eq uPred_ownM_aux. Program Definition uPred_cmra_valid_def {M} {A : cmraT} (a : A) : uPred M := {| uPred_holds n x := ✓{n} a |}. Solve Obligations with naive_solver eauto 2 using cmra_validN_le. -Definition uPred_cmra_valid_aux : { x | x = @uPred_cmra_valid_def }. by eexists. Qed. -Definition uPred_cmra_valid {M A} := proj1_sig uPred_cmra_valid_aux M A. +Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). by eexists. Qed. +Definition uPred_cmra_valid {M A} := unseal uPred_cmra_valid_aux M A. Definition uPred_cmra_valid_eq : - @uPred_cmra_valid = @uPred_cmra_valid_def := proj2_sig uPred_cmra_valid_aux. + @uPred_cmra_valid = @uPred_cmra_valid_def := seal_eq uPred_cmra_valid_aux. Program Definition uPred_bupd_def {M} (Q : uPred M) : uPred M := {| uPred_holds n x := ∀ k yf, @@ -152,9 +152,9 @@ Next Obligation. apply uPred_mono with x'; eauto using cmra_includedN_l. Qed. Next Obligation. naive_solver. Qed. -Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed. -Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M. -Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux. +Definition uPred_bupd_aux : seal (@uPred_bupd_def). by eexists. Qed. +Definition uPred_bupd {M} := unseal uPred_bupd_aux M. +Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux. (* Latest notation *) Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%C%type) @@ -194,11 +194,11 @@ Notation "P -∗ Q" := (P ⊢ Q) (at level 99, Q at level 200, right associativity) : C_scope. Module uPred. -Definition unseal := +Definition unseal_eqs := (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq, uPred_exist_eq, uPred_internal_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq, uPred_later_eq, uPred_ownM_eq, uPred_cmra_valid_eq, uPred_bupd_eq). -Ltac unseal := rewrite !unseal /=. +Ltac unseal := rewrite !unseal_eqs /=. Section primitive. Context {M : ucmraT}. diff --git a/theories/prelude/base.v b/theories/prelude/base.v index 92606a94b39483093fc2900afbeff5687503ae0f..e1c36a0aeb0ef85a6d46a9fe3033a8d54e423823 100644 --- a/theories/prelude/base.v +++ b/theories/prelude/base.v @@ -14,6 +14,13 @@ Export ListNotations. From Coq.Program Require Export Basics Syntax. Obligation Tactic := idtac. +(** Sealing off definitions *) +Set Primitive Projections. +Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }. +Arguments unseal {_ _} _. +Arguments seal_eq {_ _} _. +Unset Primitive Projections. + (** Throughout this development we use [C_scope] for all general purpose notations that do not belong to a more specific scope. *) Delimit Scope C_scope with C. diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v index 98a08018f3f570b438a5939c778eba998260d9c3..5e506c8dcdf251fa230ce68784c206196680d376 100644 --- a/theories/program_logic/weakestpre.v +++ b/theories/program_logic/weakestpre.v @@ -31,9 +31,9 @@ Qed. Definition wp_def `{irisG Λ Σ} : coPset → expr Λ → (val Λ → iProp Σ) → iProp Σ := fixpoint wp_pre. -Definition wp_aux : { x | x = @wp_def }. by eexists. Qed. -Definition wp := proj1_sig wp_aux. -Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux. +Definition wp_aux : seal (@wp_def). by eexists. Qed. +Definition wp := unseal wp_aux. +Definition wp_eq : @wp = @wp_def := seal_eq wp_aux. Arguments wp {_ _ _} _ _%E _. Instance: Params (@wp) 5. diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v index 57b08033b863fdee212183583cd1a7567b18a078..ae93137134872f3e7fffd8278f78d655c89b88d4 100644 --- a/theories/proofmode/notation.v +++ b/theories/proofmode/notation.v @@ -7,22 +7,22 @@ Arguments Envs _ _%proof_scope _%proof_scope. Arguments Enil {_}. Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope. -Notation "​" := Enil (format "​") : proof_scope. -Notation "Γ ​ H : P" := (Esnoc Γ H P) +Notation "​" := Enil (format "​", only printing) : proof_scope. +Notation "Γ H : P" := (Esnoc Γ H P) (at level 1, P at level 200, - left associativity, format "Γ ​ H : P '//'") : proof_scope. + left associativity, format "Γ H : P '//'", only printing) : proof_scope. Notation "Γ '--------------------------------------' â–¡ Δ '--------------------------------------' ∗ Q" := (of_envs (Envs Γ Δ) ⊢ Q%I) (at level 1, Q at level 200, left associativity, - format "Γ '--------------------------------------' â–¡ '//' Δ '--------------------------------------' ∗ '//' Q '//'") : + format "Γ '--------------------------------------' â–¡ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope. Notation "Δ '--------------------------------------' ∗ Q" := (of_envs (Envs Enil Δ) ⊢ Q%I) (at level 1, Q at level 200, left associativity, - format "Δ '--------------------------------------' ∗ '//' Q '//'") : C_scope. + format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope. Notation "Γ '--------------------------------------' â–¡ Q" := (of_envs (Envs Γ Enil) ⊢ Q%I) (at level 1, Q at level 200, left associativity, - format "Γ '--------------------------------------' â–¡ '//' Q '//'") : C_scope. + format "Γ '--------------------------------------' â–¡ '//' Q '//'", only printing) : C_scope. Notation "​​ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I) - (at level 1, Q at level 200, format "​​ Q") : C_scope. + (at level 1, Q at level 200, format "​​ Q", only printing) : C_scope.