confluence of parallel substitution (tps) started ...

[helm.git] / matita / matita / lib / lambda-delta / names.txt

diff --git a/matita/matita/lib/lambda-delta/names.txt b/matita/matita/lib/lambda-delta/names.txt
index 61ef3e314fea0317859ab82b85dd3c2f8bd8a10b..2a030fb4fe9e59a1f85c14272cac93d2f229a95c 100644 (file)
--- a/matita/matita/lib/lambda-delta/names.txt
+++ b/matita/matita/lib/lambda-delta/names.txt
@@ -1,8 +1,11 @@
 NAMING CONVENTIONS FOR METAVARIABLES
 
+H      : reserved: transient premise
+IH     : reserved: inductive premise
 I,J    : item
 K,L    : local environment
 T,U,V,W: term
+X,Y,Z  : reserved: transient objet denoted by a capital letter
 
 d      : relocation depth
 e      : relocation height