Add `locC`, the OFE on locations.

8d2e6a66 · Robbert Krebbers · 31aca833 · 8d2e6a66
Commit 8d2e6a66 authored Nov 26, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 0 deletions

theories/heap_lang/lang.v theories/heap_lang/lang.v +1 -0

No files found.
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -337,6 +337,7 @@ Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
 Instance expr_inhabited : Inhabited expr := populate (Val inhabitant).

 Canonical Structure stateC := leibnizC state.
+Canonical Structure locC := leibnizC loc.
 Canonical Structure valC := leibnizC val.
 Canonical Structure exprC := leibnizC expr.