From ccba6c718af6a5a15f278fc9365b6ad27108e98f Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 29 Apr 2010 16:06:42 +0000
Subject: Various minor improvements of comments in mli for ocamldoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/vm.mli | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index ff76e7cd5..cd5999f04 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -3,16 +3,18 @@ open Term
 open Cbytecodes
 open Cemitcodes
 
+(** Efficient Virtual Machine *)
 
 val set_drawinstr : unit -> unit
 
 val transp_values : unit -> bool
 val set_transp_values : bool -> unit
 
-(** le code machine *)
+(** Machine code *)
+
 type tcode
 
-(** Les valeurs ***********)
+(** Values *)
 
 type vprod
 type vfun
@@ -27,11 +29,11 @@ type atom =
   | Aiddef of id_key * values
   | Aind of inductive
 
-(** Les zippers *)
+(** Zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (** Peut-etre vide *)
+  | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -49,6 +51,7 @@ type whd =
   | Vatom_stk of atom * stack
 
 (** Constructors *)
+
 val val_of_str_const : structured_constant -> values
 
 val val_of_rel : int -> values
@@ -63,21 +66,26 @@ val val_of_constant_def : int -> constant -> values -> values
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
+
 val whd_val : values -> whd
 
 (** Arguments *)
+
 val nargs : arguments -> int
 val arg : arguments -> int -> values
 
 (** Product *)
+
 val dom : vprod -> values
 val codom : vprod -> vfun
 
 (** Function *)
+
 val body_of_vfun : int -> vfun -> values
 val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
 (** Fix *)
+
 val current_fix : vfix -> int
 val check_fix : vfix -> vfix -> bool
 val rec_args : vfix -> int array
@@ -85,22 +93,27 @@ val reduce_fix : int -> vfix -> vfun array * values array
                               (** bodies ,  types *)
 
 (** CoFix *)
+
 val current_cofix : vcofix -> int
 val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
-                                      (** bodies , types 
-   Block *)
+                                      (** bodies , types *)
+
+(** Block *)
+
 val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
 (** Switch *)
+
 val check_switch : vswitch -> vswitch -> bool
 val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
 (** Evaluation *)
+
 val whd_stack : values -> stack -> whd
 val force_whd : values -> stack -> whd
 
-- 
cgit v1.2.3