Imported Upstream version 8.5upstream/8.5

34 files changed, 165 insertions, 85 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a2cccc0e..88e1bce9 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -379,12 +379,12 @@ let fchain_flags () =
   { (default_unify_flags ()) with
     allow_K_in_toplevel_higher_order_unification = true }
 
-let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
+let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      evd = meta_merge nextclenv.evd clenv.evd;
+      evd = meta_merge ?with_univs nextclenv.evd clenv.evd;
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index eb108170..7ecc26ec 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -51,7 +51,7 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
-  ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+  ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
 (** {6 Unification with clenvs } *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index aaa49f11..8e922599 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index ea204361..00e74a24 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 9b358210..059ae54c 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 673dad55..35a3e5d8 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 107ce7f8..1dd5be0e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a00a95a2..6152826c 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3273c957..ed3a1df1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index d034b73c..ed99d3a3 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index e3caa886..68efa71e 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index 84ffda75..96655d53 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 02dbd1fd..b635cc96 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,14 +20,15 @@ let get_current_proof_name = Proof_global.get_current_proof_name
 let get_all_proof_names = Proof_global.get_all_proof_names
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
 
 let delete_proof = Proof_global.discard
 let delete_current_proof = Proof_global.discard_current
 let delete_all_proofs = Proof_global.discard_all
 
-let start_proof (id : Id.t) str sigma hyps c ?init_tac terminator =
+let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof sigma id str goals terminator;
+  Proof_global.start_proof sigma id ?pl str goals terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -54,6 +55,9 @@ let set_used_variables l =
 let get_used_variables () =
   Proof_global.get_used_variables ()
 
+let get_universe_binders () =
+  Proof_global.get_universe_binders ()
+
 exception NoSuchGoal
 let _ = Errors.register_handler begin function
   | NoSuchGoal -> Errors.error "No such goal."
@@ -139,7 +143,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
-    const, status, univs
+    const, status, fst univs
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index fc521ea4..cd899201 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -55,8 +55,10 @@ val delete_all_proofs : unit -> unit
 
 type lemma_possible_guards = Proof_global.lemma_possible_guards
 
+type universe_binders = Id.t Loc.located list
+
 val start_proof :
-  Id.t -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
+  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -121,6 +123,9 @@ val set_used_variables :
   Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> universe_binders option
+
 (** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
diff --git a/proofs/proof.ml b/proofs/proof.ml
index c7aa5bad..0489305a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index a0ed0654..5053fc7f 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c303f486..f22cdbcc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -63,14 +63,14 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Id.t Loc.located list
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
@@ -89,6 +89,7 @@ type pstate = {
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode Ephemeron.key;
+  universe_binders: universe_binders option;
 }
 
 (* The head of [!pstates] is the actual current proof, the other ones are
@@ -226,7 +227,7 @@ let disactivate_proof_mode mode =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints). *)
-let start_proof sigma id str goals terminator =
+let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -234,10 +235,11 @@ let start_proof sigma id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
-let start_dependent_proof id str goals terminator =
+let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -245,12 +247,14 @@ let start_dependent_proof id str goals terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    mode = find_proof_mode "No" } in
+    mode = find_proof_mode "No";
+    universe_binders = pl } in
   push initial_state pstates
 
 let get_used_variables () = (cur_pstate ()).section_vars
+let get_universe_binders () = (cur_pstate ()).universe_binders
 
-let proof_using_auto_clear = ref true
+let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
@@ -296,7 +300,8 @@ let get_open_goals () =
     List.length shelf
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
-  let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
+  let { pid; section_vars; strength; proof; terminator; universe_binders } =
+    cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
@@ -328,7 +333,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
-          let ctx_body = restrict_universe_context ctx used_univs_body in
+	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
+          let ctx_body = restrict_universe_context ctx used_univs in
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
@@ -362,8 +368,13 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
 	  const_entry_polymorphic = poly})
-      fpl initial_goals in
-  { id = pid; entries = entries; persistence = strength; universes = universes },
+		fpl initial_goals in
+  let binders =
+    Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
+	       universe_binders
+  in
+  { id = pid; entries = entries; persistence = strength;
+    universes = (universes, binders) },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
@@ -612,7 +623,10 @@ module Bullet = struct
 	(!current_behavior).name
       end;
       optwrite = begin fun n ->
-	current_behavior := Hashtbl.find behaviors n
+	current_behavior :=
+          try Hashtbl.find behaviors n
+          with Not_found ->
+            Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
     }
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index a2254508..7fbd183e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -55,18 +55,18 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = Evd.evar_universe_context
+type proof_universes = Evd.evar_universe_context * Universes.universe_binders option
+type universe_binders = Names.Id.t Loc.located list
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
-  (* constraints : Univ.constraints; *)
-  (** guards : lemma_possible_guards; *)
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
+		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -80,14 +80,15 @@ type closed_proof = proof_object * proof_terminator
     closing commands and the xml plugin); [terminator] is used at the
     end of the proof to close the proof. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
+  Evd.evar_map -> Names.Id.t -> ?pl:universe_binders ->
+  Decl_kinds.goal_kind -> (Environ.env * Term.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope  ->
-    proof_terminator -> unit
+  Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind ->
+  Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
   (e.g. a sublemma definition) has been run inside it. Assumes
@@ -140,6 +141,8 @@ val set_used_variables :
   Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
+val get_universe_binders : unit -> universe_binders option
+
 (**********************************************************)
 (*                                                        *)
 (*                            Proof modes                 *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 47b2b255..dd2c7b25 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index f5e2bad2..aa05f58a 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 7eed1cb3..a69645b1 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index dcf8a0fc..1bf38b69 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4fc0c164..a6d9735f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,7 +32,7 @@ type entry = (Term.constr * Term.types) list
 let proofview p =
   p.comb , p.solution
 
-let compact el { comb; solution } =
+let compact el ({ solution } as pv) =
   let nf = Evarutil.nf_evar solution in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
@@ -45,7 +45,7 @@ let compact el { comb; solution } =
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
-  new_el, { comb; solution = new_solution }
+  new_el, { pv with solution = new_solution; }
 
 
 (** {6 Starting and querying a proof view} *)
@@ -62,13 +62,13 @@ let dependent_init =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   (* Main routine *)
   let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; }
+  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
     let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = gl :: comb; }
+    entry, { solution = sol; comb = gl :: comb; shelf = [] }
   in
   fun t ->
     let entry, v = aux t in
@@ -232,6 +232,9 @@ let apply env t sp =
   match ans with
   | Nil (e, info) -> iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
+    let (status, gaveup) = status in
+    let status = (status, state.shelf, gaveup) in
+    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -578,7 +581,7 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.put initial
+  Shelf.modify (fun gls -> gls @ initial)
 
 
 (** [contained_in_info e evi] checks whether the evar [e] appears in
@@ -617,7 +620,7 @@ let shelve_unifiable =
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.put u
+  Shelf.modify (fun gls -> gls @ u)
 
 (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -639,6 +642,20 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let with_shelf tac =
+  let open Proof in
+  Pv.get >>= fun pv ->
+  let { shelf; solution } = pv in
+  Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
+  tac >>= fun ans ->
+  Pv.get >>= fun npv ->
+  let { shelf = gls; solution = sigma } = npv in
+  let gls' = Evd.future_goals sigma in
+  let fgoals = Evd.future_goals solution in
+  let pgoal = Evd.principal_future_goal solution in
+  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
+  Pv.set { npv with shelf; solution = sigma } >>
+  tclUNIT (CList.rev_append gls' gls, ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -867,7 +884,7 @@ module Unsafe = struct
   let tclSETGOALS = Comb.set
 
   let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx = 
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
@@ -1010,10 +1027,34 @@ end
 module Refine =
 struct
 
+  let extract_prefix env info =
+    let ctx1 = List.rev (Environ.named_context env) in
+    let ctx2 = List.rev (Evd.evar_context info) in
+    let rec share l1 l2 accu = match l1, l2 with
+    | d1 :: l1, d2 :: l2 ->
+      if d1 == d2 then share l1 l2 (d1 :: accu)
+      else (accu, d2 :: l2)
+    | _ -> (accu, l2)
+    in
+    share ctx1 ctx2 []
+
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
+    (** Typecheck the hypotheses. *)
+    let type_hyp (sigma, env) (na, body, t as decl) =
+      let evdref = ref sigma in
+      let _ = Typing.sort_of env evdref t in
+      let () = match body with
+      | None -> ()
+      | Some body -> Typing.check env evdref body t
+      in
+      (!evdref, Environ.push_named decl env)
+    in
+    let (common, changed) = extract_prefix env info in
+    let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+    let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+    (** Typecheck the conclusion *)
     let evdref = ref sigma in
-    let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
     let _ = Typing.sort_of env evdref (Evd.evar_concl info) in
     !evdref
 
@@ -1061,7 +1102,7 @@ struct
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.set { solution = sigma; comb; }
+    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
   end
 
   (** Useful definitions *)
@@ -1140,7 +1181,7 @@ module V82 = struct
       let sgs = CList.flatten goalss in
       let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
-      Pv.set { solution = evd; comb = sgs; }
+      Pv.set { ps with solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let (e, info) = Errors.push e in
       tclZERO ~info e
@@ -1152,7 +1193,7 @@ module V82 = struct
     Pv.modify begin fun ps ->
     let map g s = GoalV82.nf_evar s g in
     let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { solution = evd; comb = goals; }
+    { ps with solution = evd; comb = goals; }
     end
       
   let has_unresolved_evar pv =
@@ -1197,7 +1238,7 @@ module V82 = struct
 
   let of_tactic t gls =
     try
-      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 927df33a..2157459f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -303,6 +303,10 @@ val guard_no_unifiable : unit tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+(** [with_shelf tac] executes [tac] and returns its result together with the set
+    of goals shelved by [tac]. The current shelf is unchanged. *)
+val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
+
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
     is negative, then it puts the [n] last goals first.*)
 val cycle : int -> unit tactic
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 6e68cd2e..e9bc7761 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -157,8 +157,11 @@ end
 
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
-
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Goal.goal list;
+  shelf : Goal.goal list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
@@ -171,10 +174,10 @@ module P = struct
   type e = bool
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  type w = bool * Evar.t list
 
-  let wunit = true , [] , []
-  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+  let wunit = true , []
+  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
 
   type u = Info.state
 
@@ -226,19 +229,21 @@ module Env : State with type t := Environ.env = struct
 end
 
 module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s,[],[])
+  let put s = Logical.put (s, [])
 end
 
-module Shelf : Writer with type t = Evar.t list = struct
+module Shelf : State with type t = Evar.t list = struct
     (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
   type t = Evar.t list
-  let put sh = Logical.put (true,sh,[])
+  let get = Logical.map (fun {shelf} -> shelf) Pv.get
+  let set c = Pv.modify (fun pv -> { pv with shelf = c })
+  let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
 end
 
 module Giveup : Writer with type t = Evar.t list = struct
     (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
   type t = Evar.t list
-  let put gs = Logical.put (true,[],gs)
+  let put gs = Logical.put (true, gs)
 end
 
 (** Lens and utilies pertaining to the info trace *)
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index d2a2e55f..7a6ea10f 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -68,15 +68,19 @@ end
 
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Goal.goal list;
+  shelf : Goal.goal list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
 module P : sig
   type s = proofview * Environ.env
 
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  (** Status (safe/unsafe) * given up *)
+  type w = bool * Evar.t list
 
   val wunit : w
   val wprod : w -> w -> w
@@ -123,7 +127,7 @@ module Status : Writer with type t := bool
 
 (** Lens to the list of goals which have been shelved during the
     execution of the tactic. *)
-module Shelf : Writer with type t = Evar.t list
+module Shelf : State with type t = Evar.t list
 
 (** Lens to the list of goals which were given up during the execution
     of the tactic. *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b0..ea21917a 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index b32cedf8..b9191108 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ba62b2cb..14493458 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index a81555ff..13a9be59 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4238d1e3..a75b6fa0 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a0e1a015..7e943cb1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6d6215c5..a4a447e8 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index e4c0a23e..215c5b29 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)