summaryrefslogtreecommitdiff
path: root/extraction/extraction.v
diff options
context:
space:
mode:
Diffstat (limited to 'extraction/extraction.v')
-rw-r--r--extraction/extraction.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v
index cc33c98..e0f965d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -47,6 +47,9 @@ Extract Constant RTLtyping.infer_type_environment => "RTLtypingaux.infer_type_en
(* Coloring *)
Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
+(* Linearize *)
+Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
+
(* PPC *)
Extract Constant PPC.low_half_signed => "fun _ -> assert false".
Extract Constant PPC.high_half_signed => "fun _ -> assert false".