X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpolicy.txt;h=7743f9bbda954626ebb171114c749b05ce859401;hb=2e700622e2565c6695e8c1264dd4c1207896f28c;hp=9f74e233918ad99ae79f068ed4d4796e0a10ab0d;hpb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;p=helm.git

diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt
index 9f74e2339..7743f9bbd 100644
--- a/matita/matita/contribs/lambda/policy.txt
+++ b/matita/matita/contribs/lambda/policy.txt
@@ -4,16 +4,17 @@ A, B, C, D: term
 H         : transient premise
 IH        : inductive premise
 M, N      : term
+P, Q      : pointer tree
 R         : arbitrary relation
 T, U      : arbitrary small type
 
-a, b      : boolean
-d, e      : variable reference depth 
+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
 l         : arbitrary list
 m, n      : measures on terms
-p, q      : redex pointer
-r, s      : redex pointer sequence
+p, q      : pointer
+r, s      : pointer sequence
 t, u      : arbitrary element