aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-07-14 06:45:10 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-07-14 06:45:10 -0400
commitce401baf05f0228807cfe53da8d37595429a9761 (patch)
treeea066c12de226f8ffe94c12149e3daee15b05a15 /src
parentc7dc57429dc494c1f74fe73f345475a320ab10b8 (diff)
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/CStringification.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/Experiments/NewPipeline/CStringification.v
index c69a93047..bb94402f4 100644
--- a/src/Experiments/NewPipeline/CStringification.v
+++ b/src/Experiments/NewPipeline/CStringification.v
@@ -30,6 +30,7 @@ Module Compilers.
Module ToString.
Local Open Scope string_scope.
+ Local Open Scope Z_scope.
Module Import ZRange.
Module Export type.