X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2Ftxt.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2Ftxt.ml;h=bdd96bf6bd8cfb90cb3e81b6eaac48cbb381a078;hb=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;hp=6ffe592de2846ae7dd7b38234299d90a4a043b4a;hpb=5280ec9794de75e63ffc01bddf1756ebcca02be0;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml
index 6ffe592de..bdd96bf6b 100644
--- a/helm/software/lambda-delta/src/text/txt.ml
+++ b/helm/software/lambda-delta/src/text/txt.ml
@@ -15,7 +15,7 @@ type ix = int (* index *)
 
 type id = string (* identifier *)
 
-type desc = string (* description *)
+type info = string * string (* language, text *)
 
 type kind = Decl (* generic declaration *) 
           | Ax   (* axiom               *)
@@ -60,7 +60,7 @@ type command =
              | 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
+(* entity: main?, class, name, info, contents *)
+	     | Entity of bool * kind * N.level * id * info * term
 (* predefined generated entity: arguments *)
              | Generate of term list