diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-04-25 10:56:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-04-25 10:56:11 +0200 |
| commit | e34dc31ee4058c8df3ca92acb33fad153634792c (patch) | |
| tree | 3f677f21612054992d235865c8ec606b428eeade /cparser/Cleanup.ml | |
| parent | 885dc4fdc5e964637fca6913fc45b108781da8d4 (diff) | |
| download | compcert-kvx-e34dc31ee4058c8df3ca92acb33fad153634792c.tar.gz compcert-kvx-e34dc31ee4058c8df3ca92acb33fad153634792c.zip | |
Use "fix <name> <number>" instead of "fix <number>"
The "fix <number>" tactic is deprecated in Coq 8.8.0 and triggers warnings.
Diffstat (limited to 'cparser/Cleanup.ml')
0 files changed, 0 insertions, 0 deletions