summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
Diffstat (limited to 'backend')
-rw-r--r--backend/RTLtyping.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index b4702cf..24f8d7b 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -394,7 +394,7 @@ Definition type_code (e: S.typenv): res S.typenv :=
end)
f.(fn_code) (OK e).
-(** S remaining constraints *)
+(** Solve remaining constraints *)
Definition check_params_norepet (params: list reg): res unit :=
if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters").