From af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 9 Dec 2014 12:48:32 +0100
Subject: Switch the few remaining iso-latin-1 files to utf8

---
 pretyping/namegen.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/namegen.ml')

diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index a6c0149a4e..ed4bc4d394 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -176,8 +176,8 @@ let next_ident_away_from id bad =
 
 let restart_subscript id =
   if not (has_subscript id) then id else
-    (* Ce serait sans doute mieux avec quelque chose inspiré de
-     *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+    (* It would probably be better with something in the spirit of
+     *** make_ident id (Some 0) *** but compatibility would be lost... *)
     forget_subscript id
 
 let rec to_avoid id = function
-- 
cgit v1.2.3