X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Fmeta.ml;fp=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2Fmeta.ml;h=23f8f52f5b5135d41f5509620183d75ca1af7991;hb=591ffe6f23ec9d2a4d368d2c1e7b213986189e44;hp=a35ecab8bb0bc26737622366fb90d04357dfd862;hpb=876ac1889f8b11c97c8d94a0523504a0bcb70ddd;p=helm.git

diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml
index a35ecab8b..23f8f52f5 100644
--- a/helm/software/lambda-delta/toplevel/meta.ml
+++ b/helm/software/lambda-delta/toplevel/meta.ml
@@ -27,13 +27,13 @@ type id = Aut.id
 
 type qid = id * id list (* qualified identifier: name, qualifiers *)
 
-type term = Sort of bool              (* sorts: true = TYPE, false = PROP *)
-	  | LRef of int               (* local reference: de bruijn index *)
-	  | GRef of qid * term list   (* global reference: name, arguments *)
-	  | Appl of term * term       (* application: argument, function *)
-	  | Abst of id * term * term  (* abstraction: name, type, body *)
+type term = Sort of bool                  (* sorts: true = TYPE, false = PROP *)
+	  | LRef of int                   (* local reference: de bruijn index *)
+	  | GRef of int * qid * term list (* global reference: context length, name, arguments *)
+	  | Appl of term * term           (* application: argument, function *)
+	  | Abst of id * term * term      (* abstraction: name, type, body *)
 
 type pars = (qid * term) list (* parameter declarations: name, type *)
 
-(* environment: parameters, name, type, (transparent?, body) *)
-type environment = (pars * qid * term * (bool * term) option) list
+(* environment: line number, parameters, name, type, (transparent?, body) *)
+type environment = (int * pars * qid * term * (bool * term) option) list