diff options
Diffstat (limited to 'backend/RTLtyping.v')
-rw-r--r-- | backend/RTLtyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index b4702cf2..24f8d7b3 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"). |