diff options
| author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-06 17:50:04 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-06 17:50:10 +0200 |
| commit | 8dac286930288a1e7dfa39e030d58cfd5714d8d3 (patch) | |
| tree | 640e443c8b598fd62ce1cfa7312ce56f8ef9ac42 /cparser/validator/Interpreter_safe.v | |
| parent | 47f63df0a43209570de224f28cf53da6a758df16 (diff) | |
| download | compcert-8dac286930288a1e7dfa39e030d58cfd5714d8d3.tar.gz compcert-8dac286930288a1e7dfa39e030d58cfd5714d8d3.zip | |
Alphabet.v compiles even without the hints of BigNumPrelude
BigNumPrelude will soon leave Coq stdlib with the rest of the bignum
library (apart from Int31 files) to become a separate package.
With this (very minor) patch, Compcert compiles with or without
the hints declared in BigNumPrelude.
Diffstat (limited to 'cparser/validator/Interpreter_safe.v')
0 files changed, 0 insertions, 0 deletions