]>
matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/grafite_parser/grafiteParser.ml
[ IDENT "demod"
| IDENT "fast_paramod"
| IDENT "paramod"
- | IDENT "depth"
| IDENT "width"
| IDENT "size"
- | IDENT "timeout"
- | IDENT "library"
- | IDENT "type"
- | IDENT "all"
]
];
auto_params: [