diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-16 13:24:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-23 18:15:24 +0100 |
| commit | 39cbf75c554cd7e5228bd6cd962766e865c3f26b (patch) | |
| tree | c434651d7d17b9e268b053a40b676009189aca5b /man | |
| parent | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff) | |
Make some functions on terms more robust w.r.t new term constructs.
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions