From 61afb01b721d12068ade37f5c809319668e3573e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 20 Jan 2020 08:45:51 +0100
Subject: Translating a comment from French to English.

---
 tactics/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index da4de3df77..9a14f4d40f 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -362,7 +362,7 @@ let inVariable : unit -> obj =
     classify_function = (fun () -> Dispose)}
 
 let declare_variable ~name ~kind d =
-  (* Constr raisonne sur les noms courts *)
+  (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (AlreadyDeclared (None, name));
 
-- 
cgit v1.2.3