diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-03 15:13:42 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-02-03 15:13:42 +0100 |
| commit | 05eac28e5040e12d75d17c25e190dcf22ec530d7 (patch) | |
| tree | c26ab6722132cfd88288721babe360c8b4efbff7 /extraction | |
| parent | 49910cab799a752c8e2f83b33b6732b215d4e17b (diff) | |
| download | compcert-kvx-05eac28e5040e12d75d17c25e190dcf22ec530d7.tar.gz compcert-kvx-05eac28e5040e12d75d17c25e190dcf22ec530d7.zip | |
Removed Cabshelper open and avoided shadowing.
The Cabshelper is only used in 4 places, so we don't need a global
open. Furhtermore the String.t type is now inlined for Cabs to
avoid shadowing problems in Elab.ml
Bug 19872
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index ffa06ddf..82b0a023 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -124,7 +124,7 @@ Extract Constant Cabs.cabsloc => byteno: int; ident : int; }". -Extract Constant Cabs.string => "String.t". +Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". (* Int31 *) |