X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2Fbrg.ml;h=09d2f247a33f8078193cee8b688f2a1489df1b69;hb=e86383ae4805a526b3acca2ef3c936b3f22daaad;hp=a3a32f8d0fd6855a3b0d21295488e9847364d4c9;hpb=51870ae9cdf98c4f58ebf223be4c85c40d49ec85;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brg.ml b/helm/software/lambda-delta/basic_rg/brg.ml
index a3a32f8d0..09d2f247a 100644
--- a/helm/software/lambda-delta/basic_rg/brg.ml
+++ b/helm/software/lambda-delta/basic_rg/brg.ml
@@ -1,15 +1,26 @@
-module U = NUri
-module A = Aut
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.              
+     \ /   This software is distributed as is, NO WARRANTY.              
+      V_______________________________________________________________ *)
 
-type uri = U.uri
-type id = A.id
+type uri = NUri.uri
+type id = Aut.id
 
-type binder = Abst | Abbr
+type bind = Abst | Abbr (* abstraction, abbreviation *)
 
-type term = Sort of int
-          | LRef of int
-	  | GRef of uri
-	  | Cast of term * term
-	  | Appl of term * term
-	  | Bind of id * binder * term * term
-	  
+type term = Sort of int                     (* hierarchy index *)
+          | LRef of int                     (* reverse de Bruijn index *)
+	  | GRef of uri                     (* reference *)
+	  | Cast of term * term             (* type, term *)
+	  | Appl of term * term             (* argument, function *)
+	  | Bind of id * bind * term * term (* name, binder, content, scope *)
+
+type entry = uri * bind * term (* uri, binder, contents *)
+
+type item = entry option