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

diff --git a/matita/matita/contribs/lambda/policy.txt b/matita/matita/contribs/lambda/policy.txt
index 7743f9bbd..9e64369a9 100644
--- a/matita/matita/contribs/lambda/policy.txt
+++ b/matita/matita/contribs/lambda/policy.txt
@@ -1,20 +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
-T, U      : arbitrary small type
+S         : arbitrary small type
+T, U, V, W: subset of subterms
 
-c         : pointer step
+a         : arbitrary element
+b,c       : boolean mark
 d, e      : variable reference level
+f         : arbitrary function
 h         : relocation height
 i, j      : variable reference depth (de Bruijn index)
 k         : relocation height
 l         : arbitrary list
 m, n      : measures on terms
+o         : pointer step
 p, q      : pointer
 r, s      : pointer sequence
-t, u      : arbitrary element