summaryrefslogtreecommitdiff
path: root/compiler/PureToExtract.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/PureToExtract.ml')
-rw-r--r--compiler/PureToExtract.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/PureToExtract.ml b/compiler/PureToExtract.ml
index 77c3afd4..7f79aa88 100644
--- a/compiler/PureToExtract.ml
+++ b/compiler/PureToExtract.ml
@@ -137,7 +137,7 @@ type formatter = {
indices to names, the responsability of finding a proper index is
delegated to helper functions.
*)
- extract_constant_value : F.formatter -> bool -> constant_value -> unit;
+ extract_primitive_value : F.formatter -> bool -> primitive_value -> unit;
(** Format a constant value.
Inputs: