1 files changed, 36 insertions, 36 deletions

diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index d81b98ac..145ca27d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -11,15 +11,15 @@ open Cbytegen
 external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external free_tcode : tcode -> unit = "coq_static_free"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
- 
+
 (*******************)
 (* Linkage du code *)
 (*******************)
 
 (* Table des globaux *)
 
-(* [global_data] contient les valeurs des constantes globales 
-   (axiomes,definitions), les annotations des switch et les structured 
+(* [global_data] contient les valeurs des constantes globales
+   (axiomes,definitions), les annotations des switch et les structured
    constant *)
 external global_data : unit -> values array = "get_coq_global_data"
 
@@ -28,18 +28,18 @@ external realloc_global_data : int -> unit = "realloc_coq_global_data"
 
 let check_global_data n =
   if n >= Array.length (global_data()) then realloc_global_data n
-  
+
 let num_global = ref 0
 
-let set_global v = 
+let set_global v =
   let n = !num_global in
   check_global_data n;
   (global_data()).(n) <- v;
   incr num_global;
   n
 
-(* [global_transp],[global_boxed] contiennent les valeurs des 
-   definitions gelees. Les deux versions sont maintenues en //. 
+(* [global_transp],[global_boxed] contiennent les valeurs des
+   definitions gelees. Les deux versions sont maintenues en //.
    [global_transp] contient la version transparente.
    [global_boxed] contient la version gelees. *)
 
@@ -50,7 +50,7 @@ external realloc_global_boxed : int -> unit = "realloc_coq_global_boxed"
 
 let check_global_boxed n =
   if n >= Array.length (global_boxed()) then realloc_global_boxed n
-  
+
 let num_boxed = ref 0
 
 let boxed_tbl = Hashtbl.create 53
@@ -59,7 +59,7 @@ let cst_opaque = ref Cpred.full
 
 let is_opaque kn = Cpred.mem kn !cst_opaque
 
-let set_global_boxed kn v = 
+let set_global_boxed kn v =
   let n = !num_boxed in
   check_global_boxed n;
   (global_boxed()).(n) <- (is_opaque kn);
@@ -91,18 +91,18 @@ let key rk =
 
 (* slot_for_*, calcul la valeur de l'objet, la place
    dans la table global, rend sa position dans la table *)
- 
+
 let slot_for_str_cst key =
-  try Hashtbl.find str_cst_tbl key 
-  with Not_found -> 
+  try Hashtbl.find str_cst_tbl key
+  with Not_found ->
     let n = set_global (val_of_str_const key) in
     Hashtbl.add str_cst_tbl key n;
     n
 
 let slot_for_annot key =
-  try Hashtbl.find annot_tbl key 
-  with Not_found -> 
-    let n =  set_global (Obj.magic key) in
+  try Hashtbl.find annot_tbl key
+  with Not_found ->
+    let n =  set_global (val_of_annot_switch key) in
     Hashtbl.add annot_tbl key n;
     n
 
@@ -112,25 +112,25 @@ let rec slot_for_getglobal env kn =
   with NotEvaluated ->
     let pos =
       match Cemitcodes.force cb.const_body_code with
-      | BCdefined(boxed,(code,pl,fv)) -> 
+      | BCdefined(boxed,(code,pl,fv)) ->
 	let v = eval_to_patch env (code,pl,fv) in
-  	if boxed then set_global_boxed kn v 
-	else set_global v 
-    | BCallias kn' -> slot_for_getglobal env kn' 
+  	if boxed then set_global_boxed kn v
+	else set_global v
+    | BCallias kn' -> slot_for_getglobal env kn'
     | BCconstant -> set_global (val_of_constant kn) in
     rk := Some pos;
     pos
 
 and slot_for_fv env fv =
   match fv with
-  | FVnamed id -> 
+  | FVnamed id ->
       let nv = Pre_env.lookup_named_val id env in
       begin
 	match !nv with
 	| VKvalue (v,_) -> v
-	| VKnone -> 
+	| VKnone ->
 	    let (_, b, _) = Sign.lookup_named id env.env_named_context in
-	    let v,d = 
+	    let v,d =
 	      match b with
 		| None -> (val_of_named id, Idset.empty)
 		| Some c -> (val_of_constr env c, Environ.global_vars_set (Environ.env_of_pre_env env) c)
@@ -142,43 +142,43 @@ and slot_for_fv env fv =
       begin
 	match !rv with
 	| VKvalue (v, _) -> v
-	| VKnone -> 
-	    let (_, b, _) = Sign.lookup_rel i env.env_rel_context in
+	| VKnone ->
+	    let (_, b, _) = lookup_rel i env.env_rel_context in
 	    let (v, d) =
-	      match b with 
+	      match b with
 		| None -> (val_of_rel i, Idset.empty)
 		| Some c -> let renv =  env_of_rel i env in
 			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
 	    in
 	      rv := VKvalue (v,d); v
       end
- 
-and eval_to_patch env (buff,pl,fv) = 
+
+and eval_to_patch env (buff,pl,fv) =
   let patch = function
     | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a)
     | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc)
-    | Reloc_getglobal kn, pos -> 
+    | Reloc_getglobal kn, pos ->
 	patch_int buff pos (slot_for_getglobal env kn)
-  in 
+  in
   List.iter patch pl;
-  let vm_env = Array.map (slot_for_fv env) fv in 
+  let vm_env = Array.map (slot_for_fv env) fv in
   let tc = tcode_of_code buff (length buff) in
   eval_tcode tc vm_env
 
-and val_of_constr env c = 
-  let (_,fun_code,_ as ccfv) = 
-    try compile env c 
+and val_of_constr env c =
+  let (_,fun_code,_ as ccfv) =
+    try compile env c
     with e -> print_string "can not compile \n";Format.print_flush();raise e in
   eval_to_patch env (to_memory ccfv)
- 
+
 let set_transparent_const kn =
   cst_opaque := Cpred.remove kn !cst_opaque;
-  List.iter (fun n -> (global_boxed()).(n) <- false) 
+  List.iter (fun n -> (global_boxed()).(n) <- false)
     (Hashtbl.find_all boxed_tbl kn)
 
 let set_opaque_const kn =
   cst_opaque := Cpred.add kn !cst_opaque;
-  List.iter (fun n -> (global_boxed()).(n) <- true) 
+  List.iter (fun n -> (global_boxed()).(n) <- true)
     (Hashtbl.find_all boxed_tbl kn)