Skip to content

I
Iris
Commit 54d2fa74 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

remove base_logic/deprecated 

Fixes #193
parent 801a5b24
Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 17 deletions
_CoqProject
View file @ 54d2fa74
......@@ -48,7 +48,6 @@ theories/base_logic/derived.v
theories/base_logic/base_logic.v
theories/base_logic/soundness.v
theories/base_logic/double_negation.v
theories/base_logic/deprecated.v
theories/base_logic/lib/iprop.v
theories/base_logic/lib/own.v
theories/base_logic/lib/saved_prop.v
......
theories/base_logic/deprecated.v deleted 100644 → 0
View file @ 801a5b24
(*
FIXME
From iris.base_logic Require Import primitive.
Set Default Proof Using "Type".
(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
Notation "■ φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity, only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x = y⌝ instead. *)
Notation "x = y" := (uPred_pure (x%stdpp%type = y%stdpp%type)) (only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x ## y ⌝ instead. *)
Notation "x ## y" := (uPred_pure (x%stdpp%type ## y%stdpp%type)) (only parsing) : uPred_scope.
*)
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