Imported Upstream version 8.5~beta3+dfsg

1 files changed, 20 insertions, 12 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae73..98b2d6d2 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
 
 let symb_tbl = HashtblSymbol.create 211
 
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
 
 let get_value tbl i =
   match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
 
 let symbols_tbl_name = Ginternal "symbols_tbl"
 
-let get_symbols_tbl () =
+let get_symbols () =
   let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
   HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
 
@@ -477,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
   in
   Array.equal eq_branch br1 br2
 
-(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
+(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *)
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
@@ -975,7 +979,7 @@ let compile_prim decl cond paux =
 	let args = Array.map opt_prim_aux args in
 	app_prim (Coq_primitive(op,None)) args
 (*
-    TODO: check if this inling was useful
+    TODO: check if this inlining was useful
 	begin match op with
         | Int31lt -> 
            if Sys.word_size = 64 then
@@ -2008,16 +2012,20 @@ let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_allias env c in
+      let c,u = get_alias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
         || (Cmap_env.mem c const_updates)
       then init
       else
-      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t ->
+      let comp_stack, (mind_updates, const_updates) =
+	match cb.const_proj, cb.const_body with
+        | None, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+	| Some pb, _ ->
+	   let mind = pb.proj_ind in
+	   compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
@@ -2054,7 +2062,7 @@ let mk_internal_let s code =
 
 (* ML Code for conversion function *)
 let mk_conv_code env sigma prefix t1 t2 =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2076,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
   let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
   let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_norm_code env sigma prefix t =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2094,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
   let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
   let gl = List.rev (setref :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_library_header dir =
   let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
   [Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_library_native_symbols"),
     [|MLglobal (Ginternal libname)|]))]
 
 let update_location (r,v) = r := v