aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pcic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 488819bc24..e3852504a6 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -125,7 +125,7 @@ let tuple_ref dep n =
Nametab.locate (make_short_qualid id)
end
else begin
- let id = make_ident "Build_tuple_%d" (Some n) in
+ let id = make_ident "Build_tuple_" (Some n) in
if not (tuple_exists id) then tuple_n n;
Nametab.locate (make_short_qualid id)
end