X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Ftext%2Ftxt.ml;h=db92bc8ad0b1ec1dbcad9fe4e833f2a576434544;hb=1eb848417fefd0ef7436d4a89e59535baf9632c7;hp=bdd96bf6bd8cfb90cb3e81b6eaac48cbb381a078;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/text/txt.ml b/helm/software/helena/src/text/txt.ml
index bdd96bf6b..db92bc8ad 100644
--- a/helm/software/helena/src/text/txt.ml
+++ b/helm/software/helena/src/text/txt.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module N = Level
+module N = Layer
 
 type ix = int (* index *)
 
@@ -24,12 +24,14 @@ type kind = Decl (* generic declaration *)
 	  | Th   (* theorem             *)
 
 type bind = 
-(* name, real?, domain *)
-          | Abst of (id * bool * term) list 
+(* layer, name, real?, domain *)
+          | Abst of N.layer * id * bool * term
 (* name, bodies *)
-	  | Abbr of (id * term) list                  
-(* names *)
-          | Void of id list
+	  | Abbr of id * term                  
+(* name *)
+          | Void of id
+
+and lenv = bind list
 
 and term =
 (* level *)
@@ -37,19 +39,17 @@ and term =
 (* named level *)
          | NSrt of id
 (* index, offset *)
-	 | LRef of ix * ix
+	 | LRef of ix
 (* name *)
 	 | NRef of id
 (* domain, element *)
 	 | Cast of term * term
 (* arguments, function *)
-	 | Appl of term list * term
-(* level, binder, scope *)
-	 | Bind of N.level * bind * term
+	 | Appl of term * term
+(* environment, scope *)
+         | Proj of lenv * term
 (* function, arguments *)
 	 | Inst of term * term list
-(* level, strong?, label, source, target *)
-	 | Impl of N.level * bool * id * term * term
 
 type command =
 (* required files: names *)
@@ -61,6 +61,6 @@ type command =
 (* section: Some id = open, None = close last *)
 	     | Section of id option
 (* entity: main?, class, name, info, contents *)
-	     | Entity of bool * kind * N.level * id * info * term
+	     | Constant of bool * kind * id * info * term
 (* predefined generated entity: arguments *)
              | Generate of term list