diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 69034bc1..cdb1fd63 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -10,6 +10,7 @@ (* *) (* *********************************************************************) +Require List. Require Iteration. Require Floats. Require RTLgen. @@ -21,6 +22,7 @@ Require Main. Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. +Extract Inductive List.list => "list" [ "[]" "(::)" ]. (* Float *) Extract Inlined Constant Floats.float => "float". |