diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-05-18 09:58:14 +0200 |
| commit | 4663ad4b31e351e29a4d8d034ad4a961a48263f1 (patch) | |
| tree | d21554c60ed607bf8fdd1476431f9707bf882604 /extraction/extraction.v | |
| parent | 10def48b639b8e83ae6cc8bf9c14da8c12e98370 (diff) | |
| parent | 5d017f110f6c23c29a182465ab7832a944c0ba26 (diff) | |
| download | compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.tar.gz compcert-4663ad4b31e351e29a4d8d034ad4a961a48263f1.zip | |
Merge branch 'master' into json_export
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 4c400036..f7e99545 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -77,9 +77,6 @@ Extract Constant Allocation.regalloc => "Regalloc.regalloc". (* Linearize *) Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux". -(* Bounds *) -Extract Constant Bounds.mregs_of_clobber => "Machregsaux.mregs_of_clobber". - (* SimplExpr *) Extract Constant SimplExpr.first_unused_ident => "Camlcoq.first_unused_ident". Extraction Inline SimplExpr.ret SimplExpr.error SimplExpr.bind SimplExpr.bind2. |