refactoring ...

[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
deleted file mode 100644 (file)
index bdd96bf..0000000
--- a/helm/software/lambda-delta/src/text/txt.ml
+++ /dev/null
@@ -1,66 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department, University of Bologna, Italy.                     
-    ||I||                                                                
-    ||T||  HELM is free software; you can redistribute it and/or         
-    ||A||  modify it under the terms of the GNU General Public License   
-    \   /  version 2 or (at your option) any later version.              
-     \ /   This software is distributed as is, NO WARRANTY.              
-      V_______________________________________________________________ *)
-
-module N = Level
-
-type ix = int (* index *)
-
-type id = string (* identifier *)
-
-type info = string * string (* language, text *)
-
-type kind = Decl (* generic declaration *) 
-          | Ax   (* axiom               *)
-         | Cong (* conjecture          *)
-         | Def  (* generic definition  *)
-         | Th   (* theorem             *)
-
-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: main?, class, name, info, contents *)
-            | Entity of bool * kind * N.level * id * info * term
-(* predefined generated entity: arguments *)
-             | Generate of term list