diff options
| author | Vincent Laporte | 2018-09-12 12:07:15 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-12 13:26:44 +0000 |
| commit | 896c974491488925d0f8401861bf716e2f9ead57 (patch) | |
| tree | ad5b0ba9e0c6c427b17329afc7991863fa82f555 /kernel/type_errors.mli | |
| parent | e3e1f56c38f345bccf984dd6d6d86fa06e423b96 (diff) | |
Manual: fix documentation of the “fresh” tactic
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions