]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/text/txt.ml
hints polished and fixed to allow recursive inference of ext_carr
[helm.git] / helm / software / lambda-delta / src / text / txt.ml
index dbcc0675c3f2e24fa7c4e646b2e0326d05179418..a2140585a6b95713becebbca5465e25649486628 100644 (file)
@@ -40,4 +40,3 @@ type command = Require of id list                (* required files: names *)
             | 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 *)
-