From e42f4c6199db7aef6ecc77b2c83ab1332e72c7b0 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Wed, 3 Apr 2024 12:10:45 +0000
Subject: [PATCH] rephrase comments
---
src/kernel_internals/typing/rmtmps.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 960d954306a..bed60b2cb47 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -677,7 +677,7 @@ let markReferenced ast =
(* Assumption: one can order logic labels according to their visibility.
The goal of this function is to minimize name clash when the program contains
- C labels with a name that correspond to a builtin logic label. Parsing the
+ C labels with a name that corresponds to a builtin logic label. Parsing the
result should not lead to a program with a different semantics.
For example: [Here: Old: ;]
cannot be normalized into: [Here: ;]
@@ -685,7 +685,7 @@ let markReferenced ast =
The behavior is as follows:
- select a name without name clash if there is one,
- - else, order preferencer by visibility: Post > Old > Loop* > Other
+ - else, select according to visibility: Post > Old > Loop* > Other
A difference in semantics can appear if:
- there are several builtin label names with different visibilities
@@ -693,9 +693,9 @@ let markReferenced ast =
- we select a visible label from the list
By selecting the less visible we guarantee that we do not change the
- semantics: either the selected label was not visible, it is not more visible
- now, or it was already visible and thus already masked during the typing
- phase.
+ semantics: either original name did not correspond to a visible logic label,
+ and this is also the case for the selected one, or it was already masked
+ during the typing phase.
*)
let prefer ~new_label ~old_label =
--
GitLab