Skip to content
Snippets Groups Projects
Commit 1d977b49 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'fix-instance-name' into 'master'

Rename Awesome_{ne,proper} to NamespaceMap_{ne,proper}

See merge request iris/iris!356
parents 7dc625d0 38df0d21
No related branches found
No related tags found
No related merge requests found
......@@ -46,9 +46,9 @@ Instance namespace_map_dist : Dist (namespace_map A) := λ n x y,
namespace_map_data_proj x {n} namespace_map_data_proj y
namespace_map_token_proj x = namespace_map_token_proj y.
Global Instance Awesome_ne : NonExpansive2 (@NamespaceMap A).
Global Instance NamespaceMap_ne : NonExpansive2 (@NamespaceMap A).
Proof. by split. Qed.
Global Instance Awesome_proper : Proper (() ==> (=) ==> ()) (@NamespaceMap A).
Global Instance NamespaceMap_proper : Proper (() ==> (=) ==> ()) (@NamespaceMap A).
Proof. by split. Qed.
Global Instance namespace_map_data_proj_ne: NonExpansive (@namespace_map_data_proj A).
Proof. by destruct 1. Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment