diff options
| author | Théo Zimmermann | 2018-09-13 10:37:43 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-13 10:37:43 +0200 |
| commit | d3fee162c5e2f39b313cde1e1fa738480d960163 (patch) | |
| tree | 83605b102fb061645eb95f857b5250e392524a6d /kernel/term_typing.ml | |
| parent | 2a4f3a8a84b886ee8964744a66c39cc894a36993 (diff) | |
| parent | 896c974491488925d0f8401861bf716e2f9ead57 (diff) | |
Merge PR #8467: Manual: fix documentation of the “fresh” tactic
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions