aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
Diffstat (limited to 'riscV')
-rw-r--r--riscV/Asm.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v
index 1d8fda11..dc410a3b 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -369,7 +369,7 @@ lbl:
- [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
into a float register rd.
-- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
+- [Ploadsi rd fval]: similar to [Ploadli] but loads a single FP constant fval
into a float register rd.
- [Pallocframe sz pos]: in the formal semantics, this