From 058d0971b27d5f64c76d96c710eedb0eaca5c457 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 17 Jun 2013 12:37:06 +0000
Subject: Typo in comment

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2279 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/RTLtyping.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend')

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").
-- 
cgit v1.2.3