aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/TargetPrinter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/TargetPrinter.ml')
-rw-r--r--riscV/TargetPrinter.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 381f4397..72b38bcd 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -572,7 +572,7 @@ module Target : TARGET =
fprintf oc "%s annotation: %S\n" comment annot
| 2 -> let lbl = new_label () in
fprintf oc "%a: " label lbl;
- add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args
+ add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args
| _ -> assert false
end
| EF_debug(kind, txt, targs) ->