diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/vmvalues.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 5e3a3c3347..88fcb71e77 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -11,10 +11,10 @@ open Names open Univ open Constr -(*******************************************) +(********************************************) (* Initialization of the abstract machine ***) -(* Necessary for [relaccu_tbl] *) -(*******************************************) +(* Necessary for [relaccu_tbl] *) +(********************************************) external init_vm : unit -> unit = "init_coq_vm" |