diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-12 09:25:53 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-12 09:25:53 +0100 |
commit | b125afc697c1214cb329967b506a4a740a942e81 (patch) | |
tree | f42085b4b76bdd9b2987e5077e12eadd6ba5bf95 /common/Subtyping.v | |
parent | 96913f741fa9bb31502e32178d67f9efb81033c3 (diff) | |
download | compcert-b125afc697c1214cb329967b506a4a740a942e81.tar.gz compcert-b125afc697c1214cb329967b506a4a740a942e81.zip |
Do not use "Require" inside sections (#224)
This will soon be deprecated by Coq.
Manual merge of pull request #224 by vbgl. Closes: #224
Diffstat (limited to 'common/Subtyping.v')
0 files changed, 0 insertions, 0 deletions