Merge branch 'v8.5'

20 files changed, 147 insertions, 205 deletions

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index bad2ae36eb..9e243eead5 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -82,7 +82,7 @@ show that A's type is in cumululativity relation with id's type
 argument, incurring a universe constraint. To do this, one can simply
 call Typing.resolve_evars env evdref c which will do some infer_conv to
 produce the right constraints and put them in the evar_map. Of course in
-some cases you might now from an invariant that no new constraint would
+some cases you might know from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
 forgot some. As a temporary way out, [Universes.constr_of_global] allows
 you to make a constr from any non-polymorphic constant, but it will fail
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 3d688011c2..802b0f9d80 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -61,7 +61,6 @@ and ppstack s =
 and ppatom a =
   match a with
   | Aid idk -> print_idkey idk
-  | Aiddef(idk,_) -> print_string "&";print_idkey idk
   | Aind((sp,i),_) ->  print_string "Ind(";
       print_string (string_of_mind sp);
       print_string ","; print_int i;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829ab0..416e5e5329 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 
 
 value coq_global_data;
-int coq_all_transp;
 value coq_atom_tbl;
 
 int drawinstr;
@@ -117,7 +116,6 @@ value init_coq_vm(value unit) /* ML */
     init_coq_global_data(Coq_global_data_Size);
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
-    coq_all_transp = 0;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -207,18 +205,6 @@ value realloc_coq_atom_tbl(value size)            /* ML */
   return Val_unit;
 }
 
-
-value coq_set_transp_value(value transp)
-{
-  coq_all_transp = (transp == Val_true);
-  return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
-  return Val_bool(coq_all_transp);
-}
-
 value coq_set_drawinstr(value unit)
 {
   drawinstr = 1;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1590a2141d..80100da719 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -20,13 +20,12 @@
 
 
 #define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_PROJ_TAG 3
-#define ATOM_FIX_TAG 4
-#define ATOM_SWITCH_TAG 5
-#define ATOM_COFIX_TAG 6
-#define ATOM_COFIXEVALUATED_TAG 7
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_PROJ_TAG 2
+#define ATOM_FIX_TAG 3
+#define ATOM_SWITCH_TAG 4
+#define ATOM_COFIX_TAG 5
+#define ATOM_COFIXEVALUATED_TAG 6
 
 
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index a03a67db8b..8af2efc588 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -76,11 +76,7 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
-      conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
-  | _, Vatom_stk(Aiddef(_,v),stk) ->
-      conv_whd env pb k whd1 (force_whd v stk) cu
-  | Vatom_stk(Aiddef(_,v),stk), _ ->
-      conv_whd env pb k (force_whd v stk) whd2 cu
+      conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
 
   | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
   | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
@@ -97,22 +93,6 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
       if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
-  | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
-      begin
-	try
-	  if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
-	    conv_stack env k stk1 stk2 cu
-	  else raise NotConvertible
-	with NotConvertible ->
-	  if oracle_order Univ.out_punivs (oracle_of_infos !infos) 
-	    false ik1 ik2 then
-            conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
-          else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
-      end
-  | Aiddef(ik1,v1), _ ->
-      conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
-  | _, Aiddef(ik2,v2) ->
-      conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
   | Aind _, _ | Aid _, _ -> raise NotConvertible
 
 and conv_stack env k stk1 stk2 cu =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index a822f92eb3..29e2ee601d 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -20,6 +20,12 @@ external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset : Obj.t -> int = "coq_offset"
 
 let accu_tag = 0
+let max_atom_tag = 1
+let proj_tag = 2
+let fix_app_tag = 3
+let switch_tag = 4
+let cofix_tag = 5
+let cofix_evaluated_tag = 6
 
 (*******************************************)
 (* Initalization of the abstract machine ***)
@@ -29,9 +35,6 @@ external init_vm : unit -> unit = "init_coq_vm"
 
 let _ = init_vm ()
 
-external transp_values : unit -> bool = "get_coq_transp_value"
-external set_transp_values : bool -> unit = "coq_set_transp_value"
-
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
@@ -141,7 +144,6 @@ type vswitch = {
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (* Zippers *)
@@ -176,20 +178,20 @@ let rec whd_accu a stk =
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
-  | i when i <= 2 ->
+  | i when i <= max_atom_tag ->
       Vatom_stk(Obj.magic at, stk)
-  | 3 (* proj tag *) ->
+  | i when Int.equal i proj_tag ->
      let zproj = Zproj (Obj.obj (Obj.field at 0)) in
      whd_accu (Obj.field at 1) (zproj :: stk)
-  | 4 (* fix_app tag *) ->
+  | i when Int.equal i fix_app_tag ->
       let fa = Obj.field at 1 in
       let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
-  | 5 (* switch tag  *) ->
+  | i when Int.equal i switch_tag ->
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
-  | 6 (* cofix_tag *) ->
+  | i when Int.equal i cofix_tag ->
       let vcfx = Obj.obj (Obj.field at 0) in
       let to_up = Obj.obj a in
       begin match stk with
@@ -197,7 +199,7 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
-  | 7 (* cofix_evaluated_tag *) ->
+  | i when Int.equal i cofix_evaluated_tag ->
       let vcofix = Obj.obj (Obj.field at 0) in
       let res = Obj.obj a in
       begin match stk with
@@ -258,6 +260,7 @@ let arg args i =
 		("Vm.arg size = "^(string_of_int (nargs args))^
 		 " acces "^(string_of_int i))
 
+(* Apply a value to arguments contained in [vargs] *)
 let apply_arguments vf vargs =
   let n = nargs vargs in
   if Int.equal n 0 then vf
@@ -268,13 +271,14 @@ let apply_arguments vf vargs =
      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
    end
 
-let apply_vstack vf vstk =
-  let n = Array.length vstk in
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+  let n = Array.length varray in
   if Int.equal n 0 then vf
   else
     begin
       push_ra stop;
-      push_vstack vstk;
+      push_vstack varray;
       interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
     end
 
@@ -310,6 +314,15 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str)
 
 let val_of_atom a = val_of_obj (obj_of_atom a)
 
+let atom_of_proj kn v =
+  let r = Obj.new_block proj_tag 2 in
+  Obj.set_field r 0 (Obj.repr kn);
+  Obj.set_field r 1 (Obj.repr v);
+  ((Obj.obj r) : atom)
+
+let val_of_proj kn v =
+  val_of_atom (atom_of_proj kn v)
+
 module IdKeyHash =
 struct
   type t = pconstant tableKey
@@ -360,14 +373,14 @@ external closure_arity : vfun -> int = "coq_closure_arity"
 
 let body_of_vfun k vf =
   let vargs = mkrel_vstack k 1 in
-  apply_vstack (Obj.magic vf) vargs
+  apply_varray (Obj.magic vf) vargs
 
 let decompose_vfun2 k vf1 vf2 =
   let arity = min (closure_arity vf1) (closure_arity vf2) in
   assert (0 < arity && arity < Sys.max_array_length);
   let vargs = mkrel_vstack k arity in
-  let v1 = apply_vstack (Obj.magic vf1) vargs in
-  let v2 = apply_vstack (Obj.magic vf2) vargs in
+  let v1 = apply_varray (Obj.magic vf1) vargs in
+  let v2 = apply_varray (Obj.magic vf2) vargs in
   arity, v1, v2
 
 (* Functions over fixpoint *)
@@ -497,7 +510,7 @@ let reduce_cofix k vcf =
     let self = Obj.new_block accu_tag 2 in
     Obj.set_field self 0 (Obj.repr accumulate);
     Obj.set_field self 1 (Obj.repr atom);
-    apply_vstack (Obj.obj e) [|Obj.obj self|] in
+    apply_varray (Obj.obj e) [|Obj.obj self|] in
   (Array.init ndef cofix_body, ftyp)
 
 
@@ -550,62 +563,13 @@ let branch_of_switch k sw =
   in
   Array.map eval_branch sw.sw_annot.rtbl
 
-
-
-(* Evaluation *)
-
-let rec whd_stack v stk =
-  match stk with
-  | [] -> whd_val v
-  | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
-  | Zfix (f,args) :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	whd_accu (Obj.repr v) stk
-      else
-	let v', stkt =
-	  match stkt with
-	  | Zapp args' :: stkt ->
-	      push_ra stop;
-	      push_arguments args';
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args+ nargs args') in
-	      v', stkt
-	  | _ ->
-	      push_ra stop;
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args) in
-	      v', stkt
-	in
-	whd_stack v' stkt
-  | Zswitch sw :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
-	else
-	  let to_up =
-	    match whd_accu (Obj.repr v) [] with
-	    | Vcofix (_, to_up, _) -> to_up
-	    | _ -> assert false in
-	  whd_stack (apply_switch sw to_up) stkt
-      else whd_stack (apply_switch sw v) stkt
-
-let rec force_whd v stk =
-  match whd_stack v stk with
-  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
-  | res -> res
-
-
-let rec eta_stack a stk v =
+(* Apply the term represented by a under stack stk to argument v *)
+(* t = a stk --> t v *)
+let rec apply_stack a stk v =
   match stk with
-  | [] -> apply_vstack a [|v|]
-  | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v
+  | [] -> apply_varray a [|v|]
+  | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v
+  | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v
   | Zfix(f,args) :: stk ->
       let a,stk = 
 	match stk with
@@ -626,11 +590,11 @@ let rec eta_stack a stk v =
 	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
 		(nargs args) in
 	    a, stk in
-      eta_stack a stk v
+      apply_stack a stk v
   | Zswitch sw :: stk ->
-      eta_stack (apply_switch sw a) stk v
+      apply_stack (apply_switch sw a) stk v
 
-let eta_whd k whd =
+let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
   | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
@@ -649,8 +613,4 @@ let eta_whd k whd =
       push_val v;
       interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
   | Vatom_stk(a,stk) ->
-      eta_stack (val_of_atom a) stk v 
-
-
-      
-      
+      apply_stack (val_of_atom a) stk v 
diff --git a/kernel/vm.mli b/kernel/vm.mli
index d31448ee13..045d02333c 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
 open Term
 open Cbytecodes
 
-(** Efficient Virtual Machine *)
+(** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
 (** Machine code *)
 
 type tcode
@@ -25,7 +22,6 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (** Zippers *)
@@ -106,10 +102,6 @@ val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
 
+val apply_whd : int -> whd -> values
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2a4be9f31c..47d92f5e03 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1865,17 +1865,10 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
-let context_of_arsign l =
-  let (x, _) = List.fold_right
-    (fun c (x, n) ->
-       (lift_rel_context n c @ x, List.length c + n))
-    l ([], 0)
-  in x
-
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
   let subst, len =
-    List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
+    List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
 	  | Rel n when dependent tm c
@@ -1886,19 +1879,21 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
 		| IsInd (_, IndType(indf,realargs),_) ->
-		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
-		      then (n, 1) :: subst else subst
-		    in
+		    let subst, len =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
 			  | Rel n when dependent arg c ->
 			      ((n, len) :: subst, pred len)
 			  | _ -> (subst, pred len))
-			(subst, len) realargs)
+			(subst, len) realargs
+		    in
+		    let subst =
+		      if dependent tm c && List.for_all isRel realargs
+		      then (n, len) :: subst else subst
+		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      ([], nar) tomatchs arsign
+      (List.rev tomatchs) arsign ([], nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
@@ -1913,9 +1908,12 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in
+  assert (len == 0);
   let p = predicate 0 c in
-  fst (Typing.type_of (push_rel_context (context_of_arsign arsign) env) sigma p), p
-
+  let env' = List.fold_right push_rel_context arsign env in
+  try let sigma' = fst (Typing.type_of env' sigma p) in
+        Some (sigma', p)
+  with e when precatchable_exception e -> None
 
 (* Builds the predicate. If the predicate is dependent, its context is
  * made of 1+nrealargs assumptions for each matched term in an inductive
@@ -1936,11 +1934,13 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
 	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let sigma1,pred1 =
+        let p1 =
           prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
 	(* Second strategy: we build an "inversion" predicate *)
 	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	[sigma1, pred1; sigma2, pred2]
+	(match p1 with
+	 | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
+	 | None -> [sigma2, pred2])
     | None, _ ->
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
@@ -2375,6 +2375,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
     assert(Int.equal slift 0); (* we must have folded over all elements of the arity signature *)
     arsign'', allnames, nar, eqs, neqs, refls
 
+let context_of_arsign l =
+  let (x, _) = List.fold_right
+    (fun c (x, n) ->
+       (lift_rel_context n c @ x, List.length c + n))
+    l ([], 0)
+  in x
+
 let compile_program_cases loc style (typing_function, evdref) tycon env
     (predopt, tomatchl, eqns) =
   let typing_fun tycon env = function
@@ -2405,12 +2412,11 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
     | None -> let ev = mkExistential env evdref in ev, ev
     | Some t ->
 	let pred = 
-	  try
-	    let evd, pred = prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t in
-	      evdref := evd; pred
-	  with e when Errors.noncritical e ->
-	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
-	      lift nar t
+	  match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
+	  | Some (evd, pred) -> evdref := evd; pred
+	  | None ->
+	     let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
+	       lift nar t
 	in Option.get tycon, pred
   in
   let neqs, arity =
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index af640d7f34..f768e4feef 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -179,8 +179,6 @@ and nf_whd env whd typ =
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
       nf_stk env c typ stk
-  | Vatom_stk(Aiddef(idkey,v), stk) ->
-      nf_whd env (whd_stack v stk) typ
   | Vatom_stk(Aind ind, stk) ->
       nf_stk env (mkIndU ind) (type_of_ind env ind) stk
 
@@ -312,10 +310,5 @@ and nf_cofix env cf =
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env c t  =
-  let transp = transp_values () in
-  if not transp then set_transp_values true;
   let v = Vconv.val_of_constr env c in
-  let c = nf_val env v t in
-  if not transp then set_transp_values false;
-  c
-
+  nf_val env v t
diff --git a/stm/stm.ml b/stm/stm.ml
index c7836d118b..ea31e0410f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -51,7 +51,7 @@ let execution_error, execution_error_hook = Hook.make
     feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
- ~default:(fun _ -> ()) ()
+ ~default:(fun _ _ -> ()) ()
 
 include Hook
 
@@ -372,7 +372,7 @@ end = struct (* {{{ *)
          (try let n = Hashtbl.find clus c in from::n
          with Not_found -> [from]); true in
     let oc = open_out fname_dot in
-    output_string oc "digraph states {\nsplines=ortho\n";
+    output_string oc "digraph states {\n";
     Dag.iter graph (fun from cf _ l ->
       let c1 = add_to_clus_or_ids from cf in
       List.iter (fun (dest, trans) ->
@@ -736,7 +736,7 @@ end = struct (* {{{ *)
       let good_id = !cur_id in
       cur_id := Stateid.dummy;
       VCS.reached id false;
-      Hooks.(call unreachable_state id);
+      Hooks.(call unreachable_state id (e, info));
       match Stateid.get info, safe_id with
       | None, None -> iraise (exn_on id ~valid:good_id (e, info))
       | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
@@ -2405,6 +2405,9 @@ let edit_at id =
         VCS.print ();
         iraise (e, info)
 
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
 (*********************** TTY API (PG, coqtop, coqc) ***************************)
 (******************************************************************************)
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 4bad7f0a6d..18ed6fc2e8 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -83,6 +83,10 @@ val set_compilation_hints : string -> unit
 (* Reorders the task queue putting forward what is in the perspective *)
 val set_perspective : Stateid.t list -> unit
 
+type document
+val backup : unit -> document
+val restore : document -> unit
+
 (** workers **************************************************************** **)
 
 module ProofTask : AsyncTaskQueue.Task
@@ -100,7 +104,7 @@ val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
 val parse_error_hook :
   (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
 val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
-val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t
 (* ready means that master has it at hand *)
 val state_ready_hook : (Stateid.t -> unit) Hook.t
 
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895ae8..2dad962bec 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -15,6 +15,7 @@ module PriorityQueue : sig
   val pop : ?picky:('a -> bool) -> 'a t -> 'a
   val push : 'a t -> 'a -> unit
   val clear : 'a t -> unit
+  val length : 'a t -> int
 end = struct
   type 'a item = int * 'a
   type 'a rel = 'a item -> 'a item -> int
@@ -38,6 +39,7 @@ end = struct
   let set_rel rel ({ contents = (xs, _) } as t) =
     let rel (_,x) (_,y) = rel x y in
     t := (List.sort rel xs, rel)
+  let length ({ contents = (l, _) }) = List.length l
 end
 
 type 'a t = {
@@ -92,11 +94,29 @@ let push { queue = q; lock = m; cond = c; release } x =
   Condition.broadcast c;
   Mutex.unlock m
 
+let length { queue = q; lock = m } =
+  Mutex.lock m;
+  let n = PriorityQueue.length q in
+  Mutex.unlock m;
+  n
+
 let clear { queue = q; lock = m; cond = c } =
   Mutex.lock m;
   PriorityQueue.clear q;
   Mutex.unlock m
 
+let clear_saving { queue = q; lock = m; cond = c } f =
+  Mutex.lock m;
+  let saved = ref [] in
+  while not (PriorityQueue.is_empty q) do
+    let elem = PriorityQueue.pop q in
+    match f elem with
+    | Some x -> saved := x :: !saved
+    | None -> ()
+  done;
+  Mutex.unlock m;
+  List.rev !saved
+
 let is_empty { queue = q } = PriorityQueue.is_empty q
 
 let destroy tq =
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510f..1df52d2523 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -22,9 +22,12 @@ val broadcast : 'a t -> unit
 val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
 
 val clear : 'a t -> unit
+val clear_saving : 'a t -> ('a -> 'b option) -> 'b list
 val is_empty : 'a t -> bool
 
 exception BeingDestroyed
 (* Threads blocked in pop can get this exception if the queue is being
  * destroyed *)
 val destroy : 'a t -> unit
+
+val length : 'a t -> int
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index f3fe5ef75e..f39d714628 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -102,7 +102,7 @@ let out_term = function
   | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
 
 let prolog_tac l n gl =
-  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false) gl x)) l in
+  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
   let n =
     match n with
       | ArgArg n -> n
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dbb2340364..9faa96a806 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1052,7 +1052,7 @@ let default_prepare_hint_ident = Id.of_string "H"
 
 exception Found of constr * types
 
-let prepare_hint check env init (sigma,c) =
+let prepare_hint check (poly,local) env init (sigma,c) =
   let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
   (* We re-abstract over uninstantiated evars.
      It is actually a bit stupid to generalize over evars since the first
@@ -1082,15 +1082,18 @@ let prepare_hint check env init (sigma,c) =
   let c' = iter c in
     if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
-      IsConstr (c', diff)
+    if poly then IsConstr (c', diff)
+    else if local then IsConstr (c', diff)
+    else (Global.push_context_set false diff;
+	  IsConstr (c', Univ.ContextSet.empty))
 
 let interp_hints poly =
   fun h ->
   let env = (Global.env()) in
   let sigma = Evd.from_env env in
-  let f c =
+  let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-      prepare_hint true (Global.env()) Evd.empty (evd,c) in
+      prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
     Dumpglob.add_glob (loc_of_reference r) gr;
@@ -1103,7 +1106,7 @@ let interp_hints poly =
     | HintsReference c ->
       let gr = global_with_alias c in
 	(PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c -> (PathAny, poly, f c)
+    | HintsConstr c -> (PathAny, poly, f poly c)
   in
   let fres (pri, b, r) =
     let path, poly, gr = fi r in
@@ -1159,7 +1162,7 @@ let expand_constructor_hints env sigma lems =
 	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
 			      Univ.ContextSet.empty))
     | _ ->
-	[prepare_hint false env sigma (evd,lem)]) lems
+	[prepare_hint false (false,true) env sigma (evd,lem)]) lems
 
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 5a4fb77091..e25b66b27b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -151,8 +151,9 @@ val interp_hints : polymorphic -> hints_expr -> hints_entry
 
 val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
 
-val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> 
-  open_constr -> hint_term
+val prepare_hint : bool (* Check no remaining evars *) ->
+  (bool * bool) (* polymorphic or monomorphic, local or global *) ->
+  env -> evar_map -> open_constr -> hint_term
 
 (** [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v
index 6a2f9672d3..e71ddaf71f 100644
--- a/test-suite/bugs/closed/4354.v
+++ b/test-suite/bugs/closed/4354.v
@@ -3,8 +3,9 @@ Class Lift (T : Type).
 Axiom closed_increment : forall {T} {H : Lift T}, True.
 Create HintDb core.
 Lemma closed_monotonic T (H : Lift T) : True.
+Proof.
+  Set Printing Universes.
   auto using closed_increment. Show Universes.
 Qed.
-
 (* also fails with -nois, so the content of the hint database does not matter
 *)
\ No newline at end of file
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d41ecebe0d..66f1ecd786 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -235,11 +235,9 @@ let compile_files () =
 
 (*s options for the virtual machine *)
 
-let boxed_val = ref false
 let use_vm = ref false
 
 let set_vm_opt () =
-  Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
 (** Options for proof general *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 836de042bf..406aacebea 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -463,19 +463,6 @@ let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
-let map_cardinal m =
-  let i = ref 0 in
-    ProgMap.iter (fun _ _ -> incr i) m;
-    !i
-
-exception Found of program_info
-
-let map_first m =
-  try
-    ProgMap.iter (fun _ v -> raise (Found v)) m;
-    assert(false)
-  with Found x -> x
-
 let from_prg : program_info ProgMap.t ref =
   Summary.ref ProgMap.empty ~name:"program-tcc-table"
 
@@ -682,6 +669,22 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls
       prg_hook = hook;
       prg_opaque = opaque; }
 
+let map_cardinal m =
+  let i = ref 0 in
+  ProgMap.iter (fun _ v ->
+		if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m;
+  !i
+
+exception Found of program_info
+
+let map_first m =
+  try
+    ProgMap.iter (fun _ v ->
+		  if snd (Ephemeron.get v).prg_obligations > 0 then
+		    raise (Found v)) m;
+    assert(false)
+  with Found x -> x
+
 let get_prog name =
   let prg_infos = !from_prg in
     match name with
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d0e231b264..8efe3614e2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1375,15 +1375,6 @@ let _ =
       optread  = (fun () -> !Closure.share);
       optwrite = (fun b -> Closure.share := b) }
 
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "use of boxed values";
-      optkey   = ["Boxed";"Values"];
-      optread  = (fun _ -> not (Vm.transp_values ()));
-      optwrite = (fun b -> Vm.set_transp_values (not b)) }
-
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)