diff options
| author | Pierre-Marie Pédrot | 2019-06-28 22:04:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 17:38:49 +0200 |
| commit | 1f2a3fe97be66fd3201b9c98e5744953d4149b91 (patch) | |
| tree | 9e1e992d5f2f706505e4184d990f2790e41df6ca /kernel/type_errors.mli | |
| parent | f22205ee06f9170a74dc8cefba2b42deeaeb246b (diff) | |
Cleaning up the previous code by ensuring statically invariants on opaque proofs.
We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions