last commit for helena 0.8.2

[helm.git] / helm / software / helena / src / text / txt.ml

diff --git a/helm/software/helena/src/text/txt.ml b/helm/software/helena/src/text/txt.ml
index 0633d39a9116268e9828a26a3a8e18a614feebaf..db92bc8ad0b1ec1dbcad9fe4e833f2a576434544 100644 (file)
--- a/helm/software/helena/src/text/txt.ml
+++ b/helm/software/helena/src/text/txt.ml
@@ -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.layer * 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.layer * 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.layer * id * info * term
+            | Constant of bool * kind * id * info * term
 (* predefined generated entity: arguments *)
              | Generate of term list