15 files changed, 41 insertions, 49 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index bf383a33a..df5fdce75 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -903,10 +903,12 @@ value coq_interprete
 	  Alloc_small(block, 2, ATOM_PROJ_TAG);
 	  Field(block, 0) = Field(coq_global_data, *pc);
 	  Field(block, 1) = accu;
-	  /* Create accumulator */
-	  Alloc_small(accu, 2, Accu_tag);
-	  Code_val(accu) = accumulate;
-	  Field(accu, 1) = block;
+          accu = block;
+          /* Create accumulator */
+          Alloc_small(block, 2, Accu_tag);
+          Code_val(block) = accumulate;
+          Field(block, 1) = accu;
+          accu = block;
 	} else {
 	    accu = Field(accu, *pc++);
 	}
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index f9cf2691e..a705e3004 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -184,9 +184,6 @@ let rec pp_struct_const = function
 
 let pp_lbl lbl = str "L" ++ int lbl
 
-let pp_pcon (id,u) =
-  pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
-
 let pp_fv_elem = function
   | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
   | FVrel i -> str "Rel(" ++ int i ++ str ")"
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 77eac9ee9..431c914c0 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -904,10 +904,10 @@ let compile fail_on_error ?universes:(universes=0) env c =
     in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
     (if !Flags.dump_bytecode then
-      Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+      Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Feedback.msg_warning in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
 	    Id.print tname ++ str str_max_constructors));
diff --git a/kernel/closure.ml b/kernel/closure.ml
index bf3801e54..65123108f 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -45,7 +45,7 @@ let reset () =
   prune := 0
 
 let stop() =
-  msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
+  Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
 	 str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
 	 int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++
 	 str"]")
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index f7220c94a..1e132e3ab 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,7 +15,6 @@ Copcodes
 Cemitcodes
 Nativevalues
 Primitives
-Nativeinstr
 Opaqueproof
 Declareops
 Retroknowledge
diff --git a/kernel/names.ml b/kernel/names.ml
index 8e0237863..9abc9842a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -36,7 +36,7 @@ struct
 
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Feedback.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
@@ -341,7 +341,7 @@ module ModPath = struct
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
       | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
-    let rec eq d1 d2 =
+    let eq d1 d2 =
       d1 == d2 ||
       match d1,d2 with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
diff --git a/kernel/names.mli b/kernel/names.mli
index 1dfdd8290..56f0f8c60 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -766,7 +766,7 @@ val mind_of_kn : KerName.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make1] *)
 
 val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-(** @deprecated Same as [MutInd.make2] *)
+(** @deprecated Same as [MutInd.make] *)
 
 val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
 (** @deprecated Same as [MutInd.make3] *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index dabe905de..44cf21cff 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1486,8 +1486,8 @@ let optimize_stk stk =
 (** Printing to ocaml **)
 (* Redefine a bunch of functions in module Names to generate names
    acceptable to OCaml. *)
-let string_of_id s = Unicode.ascii_of_ident (string_of_id s)
-let string_of_label l = Unicode.ascii_of_ident (string_of_label l)
+let string_of_id s = Unicode.ascii_of_ident (Id.to_string s)
+let string_of_label l = string_of_id (Label.to_id l)
 
 let string_of_dirpath = function
   | [] -> "_"
@@ -1560,8 +1560,7 @@ let pp_gname fmt g =
   Format.fprintf fmt "%s" (string_of_gname g)
 
 let pp_lname fmt ln =
-  let s = Unicode.ascii_of_ident (string_of_name ln.lname) in
-  Format.fprintf fmt "x_%s_%i" s ln.luid
+  Format.fprintf fmt "x_%s_%i" (string_of_name ln.lname) ln.luid
 
 let pp_ldecls fmt ids =
   let len = Array.length ids in
@@ -1864,7 +1863,7 @@ let compile_constant env sigma prefix ~interactive con cb =
     | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1879,11 +1878,11 @@ let compile_constant env sigma prefix ~interactive con cb =
 	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("",(con,u)),code)::auxdefs)
       in
-      if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
+      if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
       code, name
     | _ -> 
         let i = push_symbol (SymbConst con) in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 7ac5b8d7b..a0ff9e123 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 open Errors
 open Names
-open Univ
 open Nativelib
 open Reduction
 open Util
@@ -135,12 +134,12 @@ let native_conv_gen pb sigma env univs t1 t2 =
   match compile ml_filename code with
   | (true, fn) ->
       begin
-        if !Flags.debug then Pp.msg_debug (Pp.str "Running test...");
+        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
         let t0 = Sys.time () in
         call_linker ~fatal:true prefix fn (Some upds);
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
@@ -150,7 +149,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
 let native_conv cv_pb sigma env t1 t2 =
   if Coq_config.no_native_compiler then begin
     let msg = "Native compiler is disabled, falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
+    Feedback.msg_warning (Pp.str msg);
     vm_conv cv_pb env t1 t2
   end
   else
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4296b73ab..5b92e9554 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -73,20 +73,20 @@ let call_compiler ml_filename =
     ::"-w"::"a"
     ::include_dirs
     @ ["-impl"; ml_filename] in
-  if !Flags.debug then Pp.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
+  if !Flags.debug then Feedback.msg_debug (Pp.str (ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
       | Unix.WEXITED n ->
-         Pp.(msg_warning (str "command exited with status " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command exited with status " ++ int n); false
       | Unix.WSIGNALED n ->
-         Pp.(msg_warning (str "command killed by signal " ++ int n)); false
+         Feedback.msg_warning Pp.(str "command killed by signal " ++ int n); false
       | Unix.WSTOPPED n ->
-         Pp.(msg_warning (str "command stopped by signal " ++ int n)); false in
+         Feedback.msg_warning Pp.(str "command stopped by signal " ++ int n); false in
     res, link_filename
   with Unix.Unix_error (e,_,_) ->
-    Pp.(msg_warning (str (Unix.error_message e)));
+    Feedback.msg_warning Pp.(str (Unix.error_message e));
     false, link_filename
 
 let compile fn code =
@@ -120,7 +120,7 @@ let call_linker ?(fatal=true) prefix f upds =
     begin
       let msg = "Cannot find native compiler file " ^ f in
       if fatal then Errors.error msg
-      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+      else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
   (try
@@ -129,8 +129,8 @@ let call_linker ?(fatal=true) prefix f upds =
    with Dynlink.Error e as exn ->
      let exn = Errors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
-     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
-     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
+     if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 9d159be64..246b00da4 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -29,13 +29,13 @@ and translate_field prefix mp env acc (l,x) =
      let con = make_con mp empty_dirpath l in
      (if !Flags.debug then
 	let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_constant_field (pre_env env) prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
 	let id = mb.mind_packets.(0).mind_typename in
 	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      compile_mind_field prefix mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
@@ -43,7 +43,7 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
@@ -51,11 +51,11 @@ and translate_field prefix mp env acc (l,x) =
 	let msg =
 	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
 	in
-	Pp.msg_debug (Pp.str msg));
+	Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
-  if !Flags.debug then Pp.msg_debug (Pp.str "Compiling library...");
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 0e56e76aa..c30789641 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -15,7 +15,6 @@
 
 open Util
 open Names
-open Univ
 open Term
 open Declarations
 open Context.Named.Declaration
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cfc286135..30a346c91 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -20,7 +20,6 @@ open Util
 open Names
 open Term
 open Vars
-open Univ
 open Environ
 open Closure
 open Esubst
@@ -177,7 +176,7 @@ let convert_instances ~flex u u' (s, check) =
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
-  | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
+  | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
     else 
       let flex = evaluable_constant cst (info_env infos) 
@@ -682,7 +681,7 @@ let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-    Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
+    Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
     gen_conv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3839135a8..6bfd2457a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -167,8 +167,10 @@ let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
-  Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-	      
+  let open Feedback in
+  Option.iter (fun state_id ->
+      feedback ~id:(State state_id) Feedback.Complete)
+
 let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 4610dbcb0..53db6f5be 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -1,13 +1,9 @@
 open Util
 open Names
-open Term
 open Environ
-open Conv_oracle
 open Reduction
-open Closure
 open Vm
 open Csymtable
-open Univ
 
 let val_of_constr env c =
   val_of_constr (pre_env env) c
@@ -189,7 +185,7 @@ let vm_conv_gen cv_pb env univs t1 t2 =
     let v2 = val_of_constr env t2 in
     fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
   with Not_found | Invalid_argument _ ->
-    (Pp.msg_warning
+    (Feedback.msg_warning
       (Pp.str "Bytecode compilation failed, falling back to default conversion");
      Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
 			    full_transparent_state env univs t1 t2)