X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2Ftxt.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2Ftxt.ml;h=6ffe592de2846ae7dd7b38234299d90a4a043b4a;hb=22fd9c98a22929f0319286c0693fcdaee43a72df;hp=a2140585a6b95713becebbca5465e25649486628;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml
index a2140585a..6ffe592de 100644
--- a/helm/software/lambda-delta/src/text/txt.ml
+++ b/helm/software/lambda-delta/src/text/txt.ml
@@ -9,6 +9,8 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module N = Level
+
 type ix = int (* index *)
 
 type id = string (* identifier *)
@@ -17,26 +19,48 @@ type desc = string (* description *)
 
 type kind = Decl (* generic declaration *) 
           | Ax   (* axiom               *)
+	  | Cong (* conjecture          *)
 	  | Def  (* generic definition  *)
 	  | Th   (* theorem             *)
 
-type bind = Abst of (id * bool * term) list (* name, real?, domain *)
-          | Abbr of (id * term) list        (* name, bodies        *)
-          | Void of id list                 (* names               *)
-
-and term = Sort of ix                      (* level                          *)
-         | NSrt of id                      (* named level                    *)
-	 | LRef of ix * ix                 (* index, offset                  *)
-	 | NRef of id                      (* name                           *)
-	 | Cast of term * term             (* domain, element                *)
-	 | Appl of term list * term        (* arguments, function            *)
-	 | Bind of bind * term             (* binder, scope                  *)
-	 | Inst of term * term list        (* function, arguments            *)
-	 | Impl of bool * id * term * term (* strong?, label, source, target *)
-
-type command = Require of id list                (* required files: names *)
-             | Graph of id                       (* hierarchy graph: name *) 
-             | Sorts of (int option * id) list   (* sorts: index, name *)
-	     | Section of id option              (* section: Some id = open, None = close last *)
-	     | Entity of kind * id * desc * term (* entity: class, name, description, contents *) 
-             | Generate of term list             (* predefined generated entity: arguments *)
+type bind = 
+(* name, real?, domain *)
+          | Abst of (id * bool * term) list 
+(* name, bodies *)
+	  | Abbr of (id * term) list                  
+(* names *)
+          | Void of id list
+
+and term =
+(* level *)
+         | Sort of ix
+(* named level *)
+         | NSrt of id
+(* index, offset *)
+	 | LRef of ix * 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
+(* 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 *)
+             | Require of id list
+(* hierarchy graph: name *)
+             | Graph of id
+(* sorts: index, name *)
+             | Sorts of (int option * id) list
+(* section: Some id = open, None = close last *)
+	     | Section of id option
+(* entity: class, name, description, contents *)
+	     | Entity of kind * N.level * id * desc * term
+(* predefined generated entity: arguments *)
+             | Generate of term list