diff options
| author | Maxime Dénès <mail@maximedenes.fr> | 2018-12-27 10:05:22 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-12-27 10:05:22 +0100 |
| commit | 459f6414ee9ba5a0a8e138ab589eb3e1b88b5daa (patch) | |
| tree | a63f4a3d67d3fb618cd16e89b94cf76d5d893566 /doc | |
| parent | 50fd8fe358b0eacb92d4cc28b6ada062e38023f5 (diff) | |
| download | compcert-kvx-459f6414ee9ba5a0a8e138ab589eb3e1b88b5daa.tar.gz compcert-kvx-459f6414ee9ba5a0a8e138ab589eb3e1b88b5daa.zip | |
Use `Program Instance` instead of `Instance` + refine mode (#261)
CompCert currently uses `Instance` in so-called "refine" mode, where
Coq drops automatically in proof mode if some members of the instance
are missing.
This mode is soon going to be turned off by default, see
https://github.com/coq/coq/pull/9270.
In order to make CompCert robust against this change, this commit
replaces those occurrences of `Instance` that use "refine" mode
with `Program Instance`.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions