diff options
| author | JPR | 2019-05-22 21:40:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 01:49:04 +0200 |
| commit | 467eb67bb960c15e1335f375af29b4121ac5262b (patch) | |
| tree | 1ad2454c535b090738748cd8123330451a498854 /kernel/cClosure.ml | |
| parent | 20a464396fd89449569dc69b8cfb37cb69766733 (diff) | |
Fixing typos - Part 2
Diffstat (limited to 'kernel/cClosure.ml')
| -rw-r--r-- | kernel/cClosure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95f88c0306..fc7d1a54f2 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) |