]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/text/txt.ml
- the text model now supports invocations of the entity generator (to
[helm.git] / helm / software / lambda-delta / text / txt.ml
index ca32a915086aac432951679f322eac9c04a12255..dbcc0675c3f2e24fa7c4e646b2e0326d05179418 100644 (file)
@@ -39,3 +39,5 @@ type command = Require of id list                (* required files: names *)
              | 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 *)
+