diff options
| -rw-r--r-- | checker/safe_typing.ml | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index a5575892f1..5e7d7f42f8 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -140,7 +140,7 @@ end = struct (get_table : unit -> table)) = (* We use an integer as a key inside the table. *) let counter = ref 0 in - (* ... but it is wrap inside a [constr_substituted]. *) + (* ... but it is wrapped inside a [constr_substituted]. *) let key_as_constr key = Declarations.from_val (Term.Rel key) in (* During the traversal, the table is implemented by a list @@ -163,7 +163,7 @@ end = struct let lightened_library = traverse_library encode_const_body library in (lightened_library, get_table ()) - (* Loading is also a traversing that decode the embedded keys that + (* Loading is also a traversing that decodes the embedded keys that are inside the [lightened_library]. If the [load_proof] flag is set, we lookup inside the table to graft the [constr_substituted]. Otherwise, we set the [const_body] field diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index e384e510ba..504bfab04b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -906,7 +906,7 @@ end = struct (get_table : unit -> table)) = (* We use an integer as a key inside the table. *) let counter = ref 0 in - (* ... but it is wrap inside a [constr_substituted]. *) + (* ... but it is wrapped inside a [constr_substituted]. *) let key_as_constr key = Declarations.from_val (Term.mkRel key) in (* During the traversal, the table is implemented by a list @@ -929,7 +929,7 @@ end = struct let lightened_library = traverse_library encode_const_body library in (lightened_library, get_table ()) - (* Loading is also a traversing that decode the embedded keys that + (* Loading is also a traversing that decodes the embedded keys that are inside the [lightened_library]. If the [load_proof] flag is set, we lookup inside the table to graft the [constr_substituted]. Otherwise, we set the [const_body] field |