diff options
| author | Hugo Herbelin | 2018-10-11 22:35:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-11 22:35:01 +0200 |
| commit | 27fd525445e8ab37e67eebfb2bca1963e33c7f64 (patch) | |
| tree | fe644d2add34b9ded615d6a3fcecd30aee502d14 /kernel/environ.ml | |
| parent | b6392038bb9e0a93b789632db351b4e8c0f116cf (diff) | |
| parent | f61c6ce423a5560cf236ed1cd07f8955bb39074f (diff) | |
Merge PR #8703: [vernac] Remove unused `start_hook` `save_hook` from Lemmas.
Diffstat (limited to 'kernel/environ.ml')
0 files changed, 0 insertions, 0 deletions