diff options
| author | Pierre-Marie Pédrot | 2019-09-26 11:14:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-26 15:29:41 +0200 |
| commit | 92006b6cc6b49ed6f892a7e5475f32ca852a9769 (patch) | |
| tree | 7884eb1bbb64981b7545fffcb8cb3f604f8a8561 /kernel/nativevalues.ml | |
| parent | 884b413e91d293a6b2009da11f2996db0654e40f (diff) | |
Implement section discharging inside kernel.
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions