aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2020-01-20 08:45:51 +0100
committerHugo Herbelin2020-01-21 00:20:49 +0100
commit61afb01b721d12068ade37f5c809319668e3573e (patch)
treeccde82e7539a31d9f8f4af031b188914b5f59f6f
parent9d88395fd25031445d463648e81c600df179cbc6 (diff)
Translating a comment from French to English.
-rw-r--r--tactics/declare.ml2
1 files changed, 1 insertions, 1 deletions
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));