Commit f15c614c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove superfluous spaces in format of WP.

parent 3c054eb5
...@@ -7,7 +7,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ) ...@@ -7,7 +7,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
format "'WP' e @ E {{ Φ } }") : uPred_scope. format "'WP' e @ E {{ Φ } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp e%E Φ) Notation "'WP' e {{ Φ } }" := (wp e%E Φ)
(at level 20, e, Φ at level 200, (at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope. format "'WP' e {{ Φ } }") : uPred_scope.
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
......
...@@ -62,7 +62,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ) ...@@ -62,7 +62,7 @@ Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
format "'WP' e @ E {{ Φ } }") : uPred_scope. format "'WP' e @ E {{ Φ } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp e Φ) Notation "'WP' e {{ Φ } }" := (wp e Φ)
(at level 20, e, Φ at level 200, (at level 20, e, Φ at level 200,
format "'WP' e {{ Φ } }") : uPred_scope. format "'WP' e {{ Φ } }") : uPred_scope.
Section wp. Section wp.
Context {Λ : language} {Σ : iFunctor}. Context {Λ : language} {Σ : iFunctor}.
......
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