Merge branch 'master' into gen_proofmode

also improve README

Naming.md

+# Naming conventions for variables/arguments/hypotheses in the Coq development
+
+## small letters
+
+* a : A = cmraT or cofeT
+* b : B = cmraT or cofeT
+* c
+* d
+* e : expr = expressions
+* f = some generic function
+* g = some generic function
+* h : heap
+* i
+* j
+* k
+* l
+* m : iGst = ghost state
+* m* = prefix for option
+* n
+* o
+* p
+* q
+* r : iRes = resources
+* s = state (STSs)
+* s = stuckness bits
+* t
+* u
+* v : val = values of language
+* w
+* x
+* y
+* z 
+
+## capital letters
+
+* A : Type, cmraT or cofeT
+* B : Type, cmraT or cofeT
+* C
+* D   
+* E : coPset = Viewshift masks
+* F = a functor
+* G
+* H = hypotheses
+* I = indexing sets
+* J
+* K : ectx = evaluation contexts
+* K = keys of a map
+* L
+* M = maps / global CMRA
+* N : namespace
+* O 
+* P : uPred, iProp or Prop
+* Q : uPred, iProp or Prop
+* R : uPred, iProp or Prop
+* S : set state = state sets in STSs
+* T : set token = token sets in STSs
+* U
+* V : abstraction of value type in frame shift assertions
+* W
+* X : sets
+* Y : sets
+* Z : sets
+
+## small greek letters
+
+* γ : gname
+* σ : state = state of language
+* φ : interpretation of STS/Auth
+
+## capital greek letters
+
+* Φ : general predicate (over uPred, iProp or Prop)
+* Ψ : general predicate (over uPred, iProp or Prop)
+
+# Naming conventions for algebraic classes in the Coq development
+
+## Suffixes
+
+* C: OFEs
+* R: cameras
+* UR: unital cameras or resources algebras
+* F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
+* G: global camera functor management
+* T: canonical structurs for algebraic classes (for example ofeT for OFEs, cmraT for cameras)

README.md

@@ -3,6 +3,10 @@
 This is the Coq development of the [Iris Project](http://iris-project.org), in
 the MoSeL version.
 
+A LaTeX version of the core logic definitions and some derived forms is
+available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
+document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+
 ## Building Iris
 
 ### Prerequisites
@@ -79,15 +83,6 @@ followed by `make build-dep`.
   infrastructure. Users of the Iris Coq library should *not* depend on these
   modules; they may change or disappear without any notice.
 
-## Further Documentation
-
-* A LaTeX version of the core logic definitions and some derived forms is
-  available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
-  document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
-* Information on how to set up your editor for unicode input and output is
-  collected in [Editor.md](Editor.md).
-* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md)
-
 ## Case Studies
 
 The following is a (probably incomplete) list of case studies that use Iris, and
@@ -102,6 +97,11 @@ that should be compatible with this version:
 
 ## Notes for Iris Developers
 
+* Information on how to set up your editor for unicode input and output is
+  collected in [Editor.md](Editor.md).
+* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md).
+* Naming conventions are documented at [Naming.md](Naming.md).
+
 ### How to update the std++ dependency
 
 * Do the change in std++, push it.

naming.txt

-== small letters ==
-a : A : cmraT or cofeT
-b : B : cmraT or cofeT
-c
-d
-e : expr = expressions
-f : some generic function
-g : some generic function
-h : heap
-i
-j
-k
-l
-m : iGst = ghost state
-m* : prefix for option
-n
-o
-p
-q
-r : iRes = resources
-s : state (STSs), stuckness bits
-t
-u
-v : val = values of language
-w
-x
-y
-z 
-
-== capital letters ==
-A : Type, cmraT or cofeT
-B : Type, cmraT or cofeT
-C
-D   
-E : coPset = Viewshift masks
-F : a functor
-G
-H : hypotheses
-I : indexing sets
-J
-K : ectx = evaluation contexts
-    keys of a map
-L
-M : maps / global CMRA
-N : namespace
-O 
-P : uPred, iProp or Prop
-Q : uPred, iProp or Prop
-R : uPred, iProp or Prop
-S : set state = state sets in STSs
-T : set token = token sets in STSs
-U
-V : abstraction of value type in frame shift assertions
-W
-X : sets
-Y : sets
-Z : sets
-
-== small greek letters ==
-γ : gname
-σ : state = state of language
-φ : interpretation of STS/Auth
-
-== capital greek letters ==
-Φ : general predicate (over uPred, iProp or Prop)
-Ψ : general predicate (over uPred, iProp or Prop)