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 b68c3a8..26cdb6d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -20,7 +20,6 @@ Require Constprop. Require Coloring. Require Allocation. Require Compiler. -Require Initializers. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -70,6 +69,7 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring". Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". (* SimplExpr *) +Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. (* Compiler *) |