diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 333c4e0591a1e..bde28faeb9daa 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -151,11 +151,11 @@ struct end -(*******************) -(* Linkage du code *) -(*******************) +(****************) +(* Code linking *) +(****************) -(* Table des globaux *) +(* Global Table *) (** [global_table] containts values of global constants, switch annotations, structure_constant and projections. *) @@ -301,7 +301,7 @@ and eval_to_patch env (code, fv) table = (* Beware, this may look like a call to [Array.map], but it's not. Calling [Array.map f] when the first argument returned by [f] is a float would lead to [vm_env] being an unboxed Double_array - (Tag_val = Double_array_tag) whereas eval_tcode expects a + (Tag_val = Double_array_tag) whereas coq_interprete expects a regular array (Tag_val = 0). See test-suite/primitive/float/coq_env_double_array.v for an actual instance. *)