X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftext%2Ftxt.ml;h=dbcc0675c3f2e24fa7c4e646b2e0326d05179418;hb=cf72398627cd1189f42c3fbb9e29fa4b32e723c8;hp=f874a273e6b40b4dfec6f246320d889ad899ebfa;hpb=93205dc852fa208b48a05757d05d9910b7d45fa1;p=helm.git

diff --git a/helm/software/lambda-delta/text/txt.ml b/helm/software/lambda-delta/text/txt.ml
index f874a273e..dbcc0675c 100644
--- a/helm/software/lambda-delta/text/txt.ml
+++ b/helm/software/lambda-delta/text/txt.ml
@@ -13,19 +13,31 @@ type ix = int (* index *)
 
 type id = string (* identifier *)
 
-type comm = string (* comment *)
+type desc = string (* description *)
 
-type bind = Abst of (id * term) list (* name, domain *)
-          | Abbr of (id * term) list (* name, bodies *)
-          | Void of id list          (* names        *)
+type kind = Decl (* generic declaration *) 
+          | Ax   (* axiom               *)
+	  | Def  (* generic definition  *)
+	  | Th   (* theorem             *)
 
-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       *)
+type bind = Abst of (id * bool * term) list (* name, real?, domain *)
+          | Abbr of (id * term) list        (* name, bodies        *)
+          | Void of id list                 (* names               *)
 
-type entity = Section of id option              (* section: Some id = open, None = close last *)
-	    | Global of bool * id * comm * term (* global entity: false = decl, true = def    *) 
+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 *)
+