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