diff options
| author | Matej Kosik | 2015-12-16 12:33:58 +0100 |
|---|---|---|
| committer | Matej Kosik | 2015-12-18 15:57:38 +0100 |
| commit | 98065338c54717fd2d7aa887e8693acdc1cff5ba (patch) | |
| tree | f7b853e054912cc582c36b50f3348950649e2bd0 /plugins/syntax | |
| parent | e181c9b043e64342c1e51763f4fe88c78bc4736d (diff) | |
COMMENTS: added to some variants of the "Constr.kind_of_term" type.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions