diff options
Diffstat (limited to 'extraction/extraction.v')
| -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 aca7102d..0f0a8637 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -111,7 +111,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.cabsloc => "{ lineno : int; filename: string; byteno: int; |