]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/text/txt.ml
Regular expressions.
[helm.git] / helm / software / lambda-delta / text / txt.ml
index 81c210852ebf924a9cc1fcce1890394d6e281bed..dbcc0675c3f2e24fa7c4e646b2e0326d05179418 100644 (file)
@@ -34,7 +34,10 @@ and term = Sort of ix                      (* level                          *)
         | Inst of term * term list        (* function, arguments            *)
         | Impl of bool * id * term * term (* strong?, label, source, target *)
 
-type command = Graph of id                       (* hierarchy graph: name *) 
+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 *)
+