Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 17 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 897464e6..3c9692a5 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,7 +20,7 @@ open Mod_subst
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant
+  | Reloc_getglobal of pconstant
 
 type patch = reloc_info * int
 
@@ -61,8 +61,7 @@ let out_word b1 b2 b3 b4 =
       then 2 * len
       else
 	if len = Sys.max_string_length
-	then raise (Invalid_argument "String.create")  (* Pas la bonne execption
-.... *)
+	then invalid_arg "String.create"  (* Pas la bonne exception .... *)
 	else Sys.max_string_length in
     let new_buffer = String.create new_len in
     String.blit !out_buffer 0 new_buffer 0 len;
@@ -97,7 +96,7 @@ let label_table  = ref ([| |] : label_definition array)
 let extend_label_table needed =
   let new_size = ref(Array.length !label_table) in
   while needed >= !new_size do new_size := 2 * !new_size done;
-  let new_table = Array.create !new_size (Label_undefined []) in
+  let new_table = Array.make !new_size (Label_undefined []) in
   Array.blit !label_table 0 new_table 0 (Array.length !label_table);
   label_table := new_table
 
@@ -148,8 +147,8 @@ and slot_for_annot a =
   enter (Reloc_annot a);
   out_int 0
 
-and slot_for_getglobal id =
-  enter (Reloc_getglobal id);
+and slot_for_getglobal p =
+  enter (Reloc_getglobal p);
   out_int 0
 
 
@@ -165,7 +164,7 @@ let emit_instr = function
       then out(opENVACC1 + n - 1)
       else (out opENVACC; out_int n)
   | Koffsetclosure ofs ->
-      if ofs = -2 || ofs = 0 || ofs = 2
+      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out (opOFFSETCLOSURE0 + ofs / 2)
       else (out opOFFSETCLOSURE; out_int ofs)
   | Kpush ->
@@ -214,7 +213,7 @@ let emit_instr = function
   | Kconst c ->
       out opGETGLOBAL; slot_for_const c
   | Kmakeblock(n, t) ->
-      if n = 0 then raise (Invalid_argument "emit_instr : block size = 0")
+      if Int.equal n 0 then invalid_arg "emit_instr : block size = 0"
       else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
       else (out opMAKEBLOCK; out_int n; out_int t)
   | Kmakeprod ->
@@ -237,7 +236,7 @@ let emit_instr = function
   | Ksetfield n ->
       if n <= 1 then out (opSETFIELD0+n)
       else (out opSETFIELD;out_int n)
-  | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
+  | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
   (* spiwack *)
   | Kbranch lbl -> out opBRANCH; out_label lbl
   | Kaddint31 -> out opADDINT31
@@ -258,6 +257,9 @@ let emit_instr = function
   | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
   | Kcompint31 -> out opCOMPINT31
   | Kdecompint31 -> out opDECOMPINT31
+  | Klorint31 -> out opORINT31
+  | Klandint31 -> out opANDINT31
+  | Klxorint31 -> out opXORINT31
   (*/spiwack *)
   | Kstop ->
       out opSTOP
@@ -276,7 +278,7 @@ let rec emit = function
       else (out opPUSHENVACC; out_int n);
       emit c
   | Kpush :: Koffsetclosure ofs :: c ->
-      if ofs = -2 || ofs = 0 || ofs = 2
+      if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
       then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
       else (out opPUSHOFFSETCLOSURE; out_int ofs);
       emit c
@@ -302,7 +304,7 @@ let rec emit = function
 
 let init () =
   out_position := 0;
-  label_table := Array.create 16 (Label_undefined []);
+  label_table := Array.make 16 (Label_undefined []);
   reloc_info := []
 
 type emitcodes = string
@@ -318,28 +320,28 @@ let rec subst_strcst s sc =
   match sc with
   | Const_sorts _ | Const_b0 _ -> sc
   | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
-  | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_ind s kn, i))
+  | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
 
 let subst_patch s (ri,pos) =
   match ri with
   | Reloc_annot a ->
       let (kn,i) = a.ci.ci_ind in
-      let ci = {a.ci with ci_ind = (subst_ind s kn,i)} in
+      let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
 
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant
+  | BCallias of pconstant
   | BCconstant
 
 let subst_body_code s = function
   | BCdefined tp -> BCdefined (subst_to_patch s tp)
-  | BCallias kn -> BCallias (fst (subst_con s kn))
+  | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
   | BCconstant -> BCconstant
 
 type to_patch_substituted = body_code substituted