diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 02:22:59 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:05:40 -0400 |
| commit | a15e584571a4e153e98a11c93d12759c45ea2dcd (patch) | |
| tree | ecb28582eef51f801e2440f715715dda1b6bb06b /kernel | |
| parent | affb6ac843380e8e134fd89380746f2f6f8c11de (diff) | |
[proof] [mutual] Factorize universe handling.
Note that we had to introduce a `restrict_ucontext` parameter to be
faithful to the implementation in obligations, however this looks like
a bug.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions