- ld-html-root: ported to permanent lambda-delta url

[helm.git] / helm / software / lambda-delta / src / text / txt.ml

diff --git a/helm/software/lambda-delta/src/text/txt.ml b/helm/software/lambda-delta/src/text/txt.ml
index 6ffe592de2846ae7dd7b38234299d90a4a043b4a..bdd96bf6bd8cfb90cb3e81b6eaac48cbb381a078 100644 (file)
--- 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