Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 30 insertions, 30 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ceba6e82..f4d0bb2b 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -1,7 +1,7 @@
 open Names
 open Term
 
-type tag = int 
+type tag = int
 
 let id_tag = 0
 let iddef_tag = 1
@@ -14,22 +14,22 @@ let cofix_evaluated_tag = 6
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of inductive
-  | Const_b0 of tag                
+  | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
 
-type reloc_table = (tag * int) array 
+type reloc_table = (tag * int) array
 
-type annot_switch = 
+type annot_switch =
    {ci : case_info; rtbl : reloc_table; tailcall : bool}
- 
-module Label = 
+
+module Label =
   struct
     type t = int
     let no = -1
     let counter = ref no
     let create () = incr counter; !counter
-    let reset_label_counter () = counter := no 
+    let reset_label_counter () = counter := no
   end
 
 
@@ -49,24 +49,24 @@ type instruction =
   | Kgrab of int                        (* number of arguments *)
   | Kgrabrec of int                     (* rec arg *)
   | Kclosure of Label.t * int           (* label, number of free variables *)
-  | Kclosurerec of int * int * Label.t array * Label.t array 
+  | Kclosurerec of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kclosurecofix of int * int * Label.t array * Label.t array 
+  | Kclosurecofix of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
   | Kgetglobal of constant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (* size, tag *)
-  | Kmakeprod 
+  | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array (* consts,blocks *)
-  | Kpushfields of int 
+  | Kpushfields of int
   | Kfield of int
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
-  | Kaddint31                           (* adds the int31 in the accu 
+  | Kaddint31                           (* adds the int31 in the accu
                                            and the one ontop of the stack *)
   | Kaddcint31                          (* makes the sum and keeps the carry *)
   | Kaddcarrycint31                     (* sum +1, keeps the carry *)
@@ -77,10 +77,10 @@ type instruction =
   | Kmulcint31                          (* multiplication, result in two
 					   int31, for exact computation *)
   | Kdiv21int31                          (* divides a double size integer
-                                           (represented by an int31 in the 
-					   accumulator and one on the top of 
+                                           (represented by an int31 in the
+					   accumulator and one on the top of
 					   the stack) by an int31. The result
-					   is a pair of the quotient and the 
+					   is a pair of the quotient and the
 					   rest.
 					   If the divisor is 0, it returns
 					   0. *)
@@ -90,11 +90,11 @@ type instruction =
 					   cycling. Takes 3 int31 i j and s,
 					   and returns x*2^s+y/(2^(31-s) *)
   | Kcompareint31                       (* unsigned comparison of int31
-					   cf COMPAREINT31 in 
+					   cf COMPAREINT31 in
 					   kernel/byterun/coq_interp.c
 					   for more info *)
   | Khead0int31                         (* Give the numbers of 0 in head of a in31*)
-  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31 
+  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31
                                            ie low bits *)
   | Kisconst of Label.t                 (* conditional jump *)
   | Kareconst of int*Label.t            (* conditional jump *)
@@ -118,19 +118,19 @@ exception NotClosed
 type vm_env = {
     size : int;              (* longueur de la liste [n] *)
     fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
-  }    
-   
-   
-type comp_env = { 
+  }
+
+
+type comp_env = {
     nb_stack : int;              (* nbre de variables sur la pile          *)
     in_stack : int list;         (* position dans la pile                  *)
     nb_rec : int;                (* nbre de fonctions mutuellement         *)
                                  (* recursives =  nbr                      *)
     pos_rec  : instruction list; (* instruction d'acces pour les variables *)
                                  (*  de point fix ou de cofix              *)
-    offset : int;                 
-    in_env : vm_env ref 
-  } 
+    offset : int;
+    in_env : vm_env ref
+  }
 
 
 
@@ -176,7 +176,7 @@ let rec instruction ppf = function
   | Kmakeprod -> fprintf ppf "\tmakeprod"
   | Kmakeswitchblock(lblt,lbls,_,sz) ->
       fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
-  | Kswitch(lblc,lblb) -> 
+  | Kswitch(lblc,lblb) ->
       fprintf ppf "\tswitch";
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
@@ -185,7 +185,7 @@ let rec instruction ppf = function
   | Kfield  n -> fprintf ppf "\tgetfield %i" n
   | Kstop -> fprintf ppf "\tstop"
   | Ksequence (c1,c2) ->
-      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
+      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
 (* spiwack *)
   | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
   | Kaddint31 -> fprintf ppf "\taddint31"
@@ -218,9 +218,9 @@ and instruction_list ppf = function
       fprintf ppf "%a@ %a" instruction instr instruction_list il
 
 
-(*spiwack: moved this type in this file  because I needed it for 
+(*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
-type block = 
+type block =
   | Bconstr of constr
   | Bstrconst of structured_constant
   | Bmakeblock of int * block array
@@ -228,10 +228,10 @@ type block =
                   (* tag , nparams, arity *)
   | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
                 (* spiwack: compilation given by a function *)
-                (* compilation function (see get_vm_constant_dynamic_info in 
+                (* compilation function (see get_vm_constant_dynamic_info in
                    retroknowledge.mli for more info) , argument array  *)
 
 
- 
+
 let draw_instr c =
   fprintf std_formatter "@[<v 0>%a@]" instruction_list c