diff options
| author | Hugo Herbelin | 2018-10-06 18:53:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-15 13:54:12 +0200 |
| commit | a52c53c166c1cc138e2e2189697d126babad1409 (patch) | |
| tree | 1f8ae18e6661be80b59ac4c3aca75b467ddb87d4 /kernel/type_errors.ml | |
| parent | 3d9080dcfa21e2afc9a9cf0ba24146b3e4341edb (diff) | |
Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.
This is a theoretical change of semantics in the presence of commands
generating a "hook", such as "Coercion c := ...", or "SubClass", or
"Canonical Structure". However, none of these commands have a
"Discharge" effect, so the case was not used.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions