lambda-delta: we added the support for position indexes in global references

[helm.git] / helm / software / lambda-delta / toplevel / meta.ml

diff --git a/helm/software/lambda-delta/toplevel/meta.ml b/helm/software/lambda-delta/toplevel/meta.ml
index a35ecab8bb0bc26737622366fb90d04357dfd862..23f8f52f5b5135d41f5509620183d75ca1af7991 100644 (file)
--- 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