X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpolicy.txt;h=33fc5979b3592672612fa9f46e970f8ef076902a;hb=f14ac9cceaaa7f1905f0dbc4548d24c4abe940e3;hp=4d6e5bd8c0017847eb4a0de80452745299992d62;hpb=5e24c923ea53c31c3e167c4ff7851877ded646c1;p=helm.git

diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt
index 4d6e5bd8c..33fc5979b 100644
--- a/matita/matita/contribs/lambda/policy.txt
+++ b/matita/matita/contribs/lambda/policy.txt
@@ -1,14 +1,24 @@
 NAMING CONVENTIONS FOR METAVARIABLES
 
 A, B, C, D: term
+F,G       : subset of subterms
 H         : transient premise
 IH        : inductive premise
 M, N      : term
+P, Q      : pointer tree
+R         : arbitrary relation
+S         : arbitrary small type
+T, U, V, W: subset of subterms
 
-a, b      : boolean
-d, e      : variable reference depth 
+a         : arbitrary element
+b         : boolean mark
+c         : pointer step
+d, e      : variable reference level
 h         : relocation height
-i, j      : de Bruijn index
+i, j      : variable reference depth (de Bruijn index)
 k         : relocation height
-p, q      : redex pointer
-r, s      : redex pointer sequence
+l         : arbitrary list
+m, n      : measures on terms
+p, q      : pointer
+r, s      : pointer sequence
+