From b2007e86b4a28570eee52439ad8b9fee603443b8 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 13:50:59 +0200
Subject: STM: Pass exception information to unreachable_state_hook functions

This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
---
 stm/stm.ml  | 4 ++--
 stm/stm.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index acbb5f646d..e96c396bae 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
 
@@ -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))
diff --git a/stm/stm.mli b/stm/stm.mli
index 4bad7f0a6d..2453f258c5 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -100,7 +100,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
 
-- 
cgit v1.2.3


From ce0c536b4430711db1e30cd7ac35ae8d71d34e64 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 13:58:50 +0200
Subject: STM: Added functions for saving and restoring the internal state

PIDEtop needs these to implement its new transaction mechanism
---
 stm/stm.ml  | 3 +++
 stm/stm.mli | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index e96c396bae..c0d71dc933 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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 2453f258c5..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
-- 
cgit v1.2.3


From 56ca108e63191e90c3d4169c37a4c97017e3c6ae Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 14:19:34 +0200
Subject: TQueue: Expose the length of TQueues

---
 stm/tQueue.ml  | 8 ++++++++
 stm/tQueue.mli | 2 ++
 2 files changed, 10 insertions(+)

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 6fef895ae8..2a43cd7d13 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,6 +94,12 @@ 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;
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
index 7458de510f..f54af4df47 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -28,3 +28,5 @@ 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
-- 
cgit v1.2.3


From f6b3704391de97ee544da9ae7316685cd2d9fae3 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 14:20:22 +0200
Subject: TQueue: Allow some tasks to be saved when clearing a TQueue

---
 stm/tQueue.ml  | 12 ++++++++++++
 stm/tQueue.mli |  1 +
 2 files changed, 13 insertions(+)

diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 2a43cd7d13..2dad962bec 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -105,6 +105,18 @@ let clear { queue = q; lock = m; cond = c } =
   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 f54af4df47..1df52d2523 100644
--- a/stm/tQueue.mli
+++ b/stm/tQueue.mli
@@ -22,6 +22,7 @@ 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
-- 
cgit v1.2.3


From 41ac12062858d3b8b82b0ed736b3800d052f34b8 Mon Sep 17 00:00:00 2001
From: Alec Faithfull
Date: Tue, 6 Oct 2015 15:23:02 +0200
Subject: STM: Work around an occasional crash in dot (debug output)

The splines=ortho option seems to make dot crash sometimes, so this commit
removes it from the STM debugging output
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index c0d71dc933..5bb46fd368 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -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) ->
-- 
cgit v1.2.3


From 864bcb82f84a8101fec9a8f7225a01083ebff8c4 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 9 Oct 2015 11:01:54 +0200
Subject: Fix inference of return clause raising a type error.

---
 pretyping/cases.ml | 54 ++++++++++++++++++++++++++++++------------------------
 1 file changed, 30 insertions(+), 24 deletions(-)

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 =
-- 
cgit v1.2.3


From d694c532f3f15569a204fa9f2d02f2c0ea83b424 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 9 Oct 2015 11:02:15 +0200
Subject: Fix Next Obligation to not raise an anomaly in case of mutual
 definitions.

---
 toplevel/obligations.ml | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 00ea2ffb84..665926922f 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"
 
@@ -680,6 +667,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
-- 
cgit v1.2.3


From f3c4dc6fb350b318ccc3af3a0e9aecb977b25744 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 9 Oct 2015 15:19:08 +0200
Subject: Fix CFGV contrib: handling of global hints introducing global
 universes.

It was wrong, the context was readded needlessly to the local evar_map context.
---
 tactics/eauto.ml4 |  2 +-
 tactics/hints.ml  | 14 ++++++++------
 tactics/hints.mli |  4 ++--
 3 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 83498cabd8..0c52968a70 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -94,7 +94,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) gl x)) l in
   let n =
     match n with
       | ArgArg n -> n
diff --git a/tactics/hints.ml b/tactics/hints.ml
index dbb2340364..e4f28b8eb2 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 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,17 @@ 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 (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 (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 +1105,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 +1161,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 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..b7b219e2e7 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -151,8 +151,8 @@ 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 (* polymorphic *) ->
+  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;
-- 
cgit v1.2.3


From 5e1296a5cae4ae0ab84ddbe7b0ec71959861af97 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 9 Oct 2015 15:41:48 +0200
Subject: Refine fix for handling of the universe contexts of hints, depending
 on their polymorphic status _and_ locality.

---
 tactics/eauto.ml4             | 2 +-
 tactics/hints.ml              | 7 ++++---
 tactics/hints.mli             | 3 ++-
 test-suite/bugs/closed/4354.v | 3 ++-
 4 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 0c52968a70..b6b18719c0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -94,7 +94,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 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 e4f28b8eb2..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 poly 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
@@ -1083,6 +1083,7 @@ let prepare_hint check poly env init (sigma,c) =
     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
     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))
 
@@ -1092,7 +1093,7 @@ let interp_hints poly =
   let sigma = Evd.from_env env in
   let f poly c =
     let evd,c = Constrintern.interp_open_constr env sigma c in
-      prepare_hint true poly (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;
@@ -1161,7 +1162,7 @@ let expand_constructor_hints env sigma lems =
 	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
 			      Univ.ContextSet.empty))
     | _ ->
-	[prepare_hint false 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 b7b219e2e7..e25b66b27b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -151,7 +151,8 @@ 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 *) -> bool (* polymorphic *) ->
+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)].
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
-- 
cgit v1.2.3


From 7c82718f18afa3b317873f756a8801774ef64061 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:19:20 +0200
Subject: Minor typo in universe polymorphism doc.

---
 dev/doc/univpoly.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3


From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 dev/vm_printers.ml          |   1 -
 kernel/byterun/coq_memory.c |  14 ------
 kernel/byterun/coq_values.h |  13 +++---
 kernel/vconv.ml             |  22 +--------
 kernel/vm.ml                | 110 ++++++++++++--------------------------------
 kernel/vm.mli               |  14 ++----
 pretyping/vnorm.ml          |   9 +---
 toplevel/coqtop.ml          |   2 -
 toplevel/vernacentries.ml   |   9 ----
 9 files changed, 41 insertions(+), 153 deletions(-)

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..4607ad7165 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
 
@@ -360,14 +364,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 +501,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 +554,12 @@ 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
   | Zfix(f,args) :: stk ->
       let a,stk = 
 	match stk with
@@ -626,11 +580,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 +603,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/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/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9b5a09de0e..8925bbe299 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/vernacentries.ml b/toplevel/vernacentries.ml
index 820903c417..35730eea03 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) *)
 
-- 
cgit v1.2.3


From db06a1ddee4c79ea8f6903596284df2f2700ddac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:20:45 +0200
Subject: Complete handling of primitive projections in VM.

This commit is a follow-up to a51cce369b9c634a93120092d4c7685a242d55b1
---
 kernel/vm.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/kernel/vm.ml b/kernel/vm.ml
index 4607ad7165..29e2ee601d 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -314,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
@@ -560,6 +569,7 @@ let rec apply_stack a stk v =
   match stk with
   | [] -> 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
-- 
cgit v1.2.3