We are decapitalizing the contributions' names ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / names.txt

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt
deleted file mode 100644 (file)
index dfa83eb..0000000
--- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt
+++ /dev/null
@@ -1,40 +0,0 @@
-NAMING CONVENTIONS FOR METAVARIABLES
-
-A,B    : arity
-C,D    : candidate of reducibility
-E,F    : RTM environment
-G      : global environment 
-H      : reserved: transient premise
-IH     : reserved: inductive premise
-I,J    : item
-K,L    : local environment
-M,N    : reserved: future use
-O      : 
-P,Q    : reserved: future use
-R      : generic predicate (relation)
-S      : RTM stack
-T,U,V,W: term
-X,Y,Z  : reserved: transient objet denoted by a capital letter
-
-d      : relocation depth
-e      : relocation height
-h      : sort hierarchy parameter
-i,j    : local reference position index (de Bruijn's)
-k      : sort index
-p,q    : global reference position
-t,u    : local reference position level (de Bruijn's)
-x,y,z  : reserved: transient objet denoted by a small letter
-
-NAMING CONVENTIONS FOR CONSTRUCTORS
-
-0: atomic
-2: binary
-
-A: application to vector
-
-a: application
-b: binder
-d: abbreviation
-f: flat
-l: abstraction
-t: native type annotation