Imported Upstream version 8.5~beta3+dfsg

21 files changed, 371 insertions, 307 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2c9c695b..a2cccc0e 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -28,7 +28,7 @@ open Misctypes
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 18883df2..aaa49f11 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -125,7 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when Errors.noncritical e ->
-      (** This is Tacticals.tclFAIL *)
-      Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
+    with e when Errors.noncritical e -> Proofview.tclZERO e
   end
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index c8cb1d1c..9b358210 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Names
 open Evd
 open Evarutil
 open Evarsolve
+open Pp
 
 (******************************************)
 (* Instantiation of existential variables *)
@@ -54,8 +55,8 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
     with e when Errors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err_loc
-        (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
-			string_of_existential evk))
+        (loc,"", str "Instance is not well-typed in the environment of " ++
+                 str (string_of_existential evk))
   in
   define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8206ca1..3273c957 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -83,7 +83,7 @@ let apply_to_hyp sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma c in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -179,7 +179,8 @@ let check_decl_position env sign (x,_,_ as d) =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    error ("Cannot create self-referring hypothesis "^Id.to_string x);
+    errorlabstrm "Logic.check_decl_position"
+      (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
 (* Auxiliary functions for primitive MOVE tactic
@@ -316,7 +317,7 @@ let meta_free_prefix a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then type_of env sigma c
+  if !check then unsafe_type_of env sigma c
   else Retyping.get_type_of env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
@@ -355,9 +356,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       | App (f,l) ->
 	let (acc',hdty,sigma,applicand) =
 	  if is_template_polymorphic env f then
-	    let sigma, ty = 
+	    let ty = 
 	      (* Template sort-polymorphism of definition and inductive types *)
-	      type_of_global_reference_knowing_conclusion env sigma f conclty
+	      let firstmeta = Array.findi (fun i x -> occur_meta x) l in
+	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
+	        type_of_global_reference_knowing_parameters env sigma f args
 	    in
 	      goalacc, ty, sigma, f
 	  else
@@ -488,9 +491,11 @@ let convert_hyp check sign sigma (id,b,bt as d) =
       (fun _ (_,c,ct) _ ->
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  error ("Incorrect change of the type of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  error ("Incorrect change of the body of "^(Id.to_string id)^".");
+	  errorlabstrm "Logic.convert_hyp"
+            (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
   reorder_val_context env sign' !reorder
@@ -522,7 +527,8 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      error ("Variable " ^ Id.to_string id ^ " is already declared.");
+	      errorlabstrm "Logic.prim_refiner"
+                (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
@@ -550,11 +556,10 @@ let prim_refiner r sigma goal =
 	  | (f,n,ar)::oth ->
 	      let ((sp',_),u')  = check_ind env n ar in
 	      if not (eq_mind sp sp') then
-		error ("Fixpoints should be on the same " ^
-		       "mutual inductive declaration.");
+		error "Fixpoints should be on the same mutual inductive declaration.";
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error
-		  ("Name "^Id.to_string f^" already used in the environment");
+		errorlabstrm "Logic.prim_refiner"
+		  (str "Name " ++ pr_id f ++ str " already used in the environment");
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] ->
 	      Evd.Monad.List.map (fun (_,_,c) sigma ->
@@ -584,8 +589,7 @@ let prim_refiner r sigma goal =
 		try
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found ->
-		  error ("All methods must construct elements " ^
-			  "in coinductive types.")
+		  error "All methods must construct elements in coinductive types."
 	in
 	let firsts,lasts = List.chop j others in
 	let all = firsts@(f,cl)::lasts in
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index d509670e..e3caa886 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -94,10 +94,6 @@ struct
 
   let print_char = fun c -> (); fun () -> print_char c
 
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
-    let (e, info) = Errors.push e in raise ~info e ()
-
   let timeout = fun n t -> (); fun () ->
     Control.timeout n t (Exception Timeout)
 
@@ -107,6 +103,13 @@ struct
       let (e, info) = Errors.push e in
       Util.iraise (Exception e, info)
 
+  (** Use the current logger. The buffer is also flushed. *)
+  let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+  let print_info s =  make (fun _ -> Pp.msg_info s;Pp.pp_flush ())
+  let print_warning s =  make (fun _ -> Pp.msg_warning s;Pp.pp_flush ())
+  let print_error s =  make (fun _ -> Pp.msg_error s;Pp.pp_flush ())
+  let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ())
+
   let run = fun x ->
     try x () with Exception e as src ->
       let (src, info) = Errors.push src in
@@ -184,7 +187,7 @@ struct
       shape of the monadic type is reminiscent of that of the
       continuation monad transformer.
 
-      The paper also contains the rational for the [split] abstraction.
+      The paper also contains the rationale for the [split] abstraction.
 
       An explanation of how to derive such a monad from mathematical
       principles can be found in "Kan Extensions for Program
@@ -208,118 +211,110 @@ struct
   type rich_exn = Exninfo.iexn
 
   type 'a iolist =
-      { iolist : 'r. (rich_exn -> 'r NonLogical.t) ->
-                     ('a -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
-                     'r NonLogical.t }
+    { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) ->
+      ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) ->
+      'r NonLogical.t }
 
   include Monad.Make(struct
-    type 'a t = state -> ('a * state) iolist
 
-    let return x : 'a t = (); fun s ->
-      { iolist = fun nil cons -> cons (x, s) nil }
+    type 'a t = 'a iolist
+
+    let return x =
+      { iolist = fun s nil cons -> cons x s nil }
 
-    let (>>=) (m : 'a t) (f : 'a -> 'b t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun (x, s) next -> (f x s).iolist next cons) }
+    let (>>=) m f =
+      { iolist = fun s nil cons ->
+        m.iolist s nil (fun x s next -> (f x).iolist s next cons) }
 
-    let (>>) (m : unit t) (f : 'a t) : 'a t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons ->
-        m.iolist nil (fun ((), s) next -> (f s).iolist next cons) }
+    let (>>) m f =
+      { iolist = fun s nil cons ->
+        m.iolist s nil (fun () s next -> f.iolist s next cons) }
 
-    let map (f : 'a -> 'b) (m : 'a t) : 'b t = (); fun s ->
-      let m = m s in
-      { iolist = fun nil cons -> m.iolist nil (fun (x, s) next -> cons (f x, s) next) }
+    let map f m =
+      { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) }
 
   end)
 
-  let zero e : 'a t = (); fun s ->
-    { iolist = fun nil cons -> nil e }
+  let zero e =
+    { iolist = fun _ nil cons -> nil e }
 
-  let plus m1 m2 : 'a t = (); fun s ->
-    let m1 = m1 s in
-    { iolist = fun nil cons -> m1.iolist (fun e -> (m2 e s).iolist nil cons) cons }
+  let plus m1 m2 =
+    { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons }
 
-  let ignore (m : 'a t) : unit t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun (_, s) next -> cons ((), s) next) }
+  let ignore m =
+    { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) }
 
-  let lift (m : 'a NonLogical.t) : 'a t = (); fun s ->
-    { iolist = fun nil cons -> NonLogical.(m >>= fun x -> cons (x, s) nil) }
+  let lift m =
+    { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) }
 
   (** State related *)
 
-  let get : P.s t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.sstate, s) nil }
+  let get =
+    { iolist = fun s nil cons -> cons s.sstate s nil }
 
-  let set (sstate : P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate }) nil }
+  let set (sstate : P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate } nil }
 
-  let modify (f : P.s -> P.s) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with sstate = f s.sstate }) nil }
+  let modify (f : P.s -> P.s) =
+    { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil }
 
-  let current : P.e t = (); fun s ->
-    { iolist = fun nil cons -> cons (s.rstate, s) nil }
+  let current =
+    { iolist = fun s nil cons -> cons s.rstate s nil }
 
-  let local (type a) (e:P.e) (m:a t) : a t = (); fun s ->
-    let m = m { s with rstate = e } in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun (x,s') next -> cons (x,{s' with rstate=s.rstate}) next) }
+  let local e m =
+    { iolist = fun s nil cons ->
+      m.iolist { s with rstate = e } nil
+        (fun x s' next -> cons x {s' with rstate = s.rstate} next) }
 
-  let put (w : P.w) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with wstate = P.wprod s.wstate w }) nil }
+  let put w =
+    { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil }
 
-  let update (f : P.u -> P.u) : unit t = (); fun s ->
-    { iolist = fun nil cons -> cons ((), { s with ustate = f s.ustate }) nil }
+  let update (f : P.u -> P.u) =
+    { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil }
 
   (** List observation *)
 
-  let once (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons -> m.iolist nil (fun x _ -> cons x nil) }
+  let once m =
+    { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) }
 
-  let break (f : rich_exn -> rich_exn option) (m : 'a t) : 'a t = (); fun s ->
-    let m = m s in
-    { iolist = fun nil cons ->
-      m.iolist nil (fun x next -> cons x (fun e -> match f e with None -> next e | Some e -> nil e))
+  let break f m =
+    { iolist = fun s nil cons ->
+      m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e))
     }
 
   (** For [reflect] and [split] see the "Backtracking, Interleaving,
       and Terminating Monad Transformers" paper.  *)
   type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t
 
-  let rec reflect (m : 'a reified) : 'a iolist =
-    { iolist = fun nil cons ->
+  let rec reflect (m : ('a * state) reified) : 'a iolist =
+    { iolist = fun s0 nil cons ->
       let next = function
       | Nil e -> nil e
-      | Cons (x, l) -> cons x (fun e -> (reflect (l e)).iolist nil cons)
+      | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons)
       in
       NonLogical.(m >>= next)
     }
 
-  let split (m : 'a t) : ('a, rich_exn -> 'a t) list_view t = (); fun s ->
-    let m = m s in
+  let split m : ('a, rich_exn -> 'a t) list_view t =
     let rnil e = NonLogical.return (Nil e) in
-    let rcons p l = NonLogical.return (Cons (p, l)) in
-    { iolist = fun nil cons ->
+    let rcons p s l = NonLogical.return (Cons ((p, s), l)) in
+    { iolist = fun s nil cons ->
       let open NonLogical in
-      m.iolist rnil rcons >>= begin function
-      | Nil e -> cons (Nil e, s) nil
+      m.iolist s rnil rcons >>= begin function
+      | Nil e -> cons (Nil e) s nil
       | Cons ((x, s), l) ->
-        let l e = (); fun _ -> reflect (l e) in
-        cons (Cons (x, l), s) nil
+        let l e = reflect (l e) in
+        cons (Cons (x, l)) s nil
       end }
 
   let run m r s =
     let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in
-    let m = m s in
     let rnil e = NonLogical.return (Nil e) in
-    let rcons (x, s) l =
+    let rcons x s l =
       let p = (x, s.sstate, s.wstate, s.ustate) in
       NonLogical.return (Cons (p, l))
     in
-    m.iolist rnil rcons
+    m.iolist s rnil rcons
 
   let repr x = x
 
diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli
index ab729aff..84ffda75 100644
--- a/proofs/logic_monad.mli
+++ b/proofs/logic_monad.mli
@@ -55,8 +55,13 @@ module NonLogical : sig
 
   val read_line : string t
   val print_char : char -> unit t
-  (** {!Pp.pp}. The buffer is also flushed. *)
-  val print : Pp.std_ppcmds -> unit t
+
+  (** Loggers. The buffer is also flushed. *)
+  val print_debug : Pp.std_ppcmds -> unit t
+  val print_warning : Pp.std_ppcmds -> unit t
+  val print_notice : Pp.std_ppcmds -> unit t
+  val print_info : Pp.std_ppcmds -> unit t
+  val print_error : Pp.std_ppcmds -> unit t
 
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d1b6afe2..02dbd1fd 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -42,7 +42,7 @@ let cook_this_proof p =
 
 let cook_proof () =
   cook_this_proof (fst
-    (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
+    (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
@@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     let () =
       match info_lvl with
       | None -> ()
-      | Some i -> Pp.ppnl (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
+      | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info))
     in
     (p,status)
   with
@@ -133,7 +133,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  let evd = Evd.from_env ~ctx Environ.empty_env in
+  let evd = Evd.from_ctx ctx in
   start_proof id goal_kind evd sign typ (fun _ -> ());
   try
     let status = by tac in
@@ -145,16 +145,20 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
-  let ce = Term_typing.handle_entry_side_effects env ce in
+  let ce =
+    if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
+    else { ce with
+      const_entry_body = Future.chain ~pure:true ce.const_entry_body
+        (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in
   let (cb, ctx), se = Future.force ce.const_entry_body in
-  assert(Declareops.side_effects_is_empty se);
-  assert(Univ.ContextSet.is_empty ctx);
-  cb, status, univs
+  let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
+  assert(Safe_typing.empty_private_constants = se);
+  cb, status, Evd.evar_universe_context univs'
 
 let refine_by_tactic env sigma ty tac =
   (** Save the initial side-effects to restore them afterwards. We set the
@@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac =
       other goals that were already present during its invocation, so that
       those goals rely on effects that are not present anymore. Hopefully,
       this hack will work in most cases. *)
-  let ans = Term_typing.handle_side_effects env ans neff in
+  let ans = Safe_typing.inline_private_constants_in_constr env ans neff in
   ans, sigma
 
 (**********************************************************************)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5e0fb4dd..fc521ea4 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -69,11 +69,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
@@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit
 (** {6 ... } *)
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
-val set_used_variables : Id.t list -> Context.section_context
+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 ... } *)
@@ -151,9 +152,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 val build_constant_by_tactic :
   Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind ->
   types -> unit Proofview.tactic -> 
-  Entries.definition_entry * bool * Evd.evar_universe_context
+  Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : env -> Evd.evar_universe_context -> ?poly:polymorphic -> 
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 828f9fa7..c7aa5bad 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -111,6 +111,8 @@ type proof = {
   shelf : Goal.goal list;
   (* List of goals that have been given up *)
   given_up : Goal.goal list;
+  (* The initial universe context (for the statement) *)
+  initial_euctx : Evd.evar_universe_context
 }
 
 (*** General proof functions ***)
@@ -171,6 +173,12 @@ let is_done p =
 (* spiwack: for compatibility with <= 8.2 proof engine *)
 let has_unresolved_evar p =
   Proofview.V82.has_unresolved_evar p.proofview
+let has_shelved_goals p = not (CList.is_empty (p.shelf))
+let has_given_up_goals p = not (CList.is_empty (p.given_up))
+
+let is_complete p =
+  is_done p && not (has_unresolved_evar p) &&
+  not (has_shelved_goals p) && not (has_given_up_goals p)
 
 (* Returns the list of partial proofs to initial goals *)
 let partial_proof p = Proofview.partial_proof p.entry p.proofview
@@ -271,7 +279,9 @@ let start sigma goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 let dependent_start goals =
   let entry, proofview = Proofview.dependent_init goals in
@@ -280,7 +290,9 @@ let dependent_start goals =
     entry;
     focus_stack = [] ;
     shelf = [] ;
-    given_up = [] } in
+    given_up = [];
+    initial_euctx =
+      Evd.evar_universe_context (snd (Proofview.proofview proofview)) } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
@@ -299,9 +311,9 @@ end
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
-  else if not (CList.is_empty (p.shelf)) then
+  else if has_shelved_goals p then
     raise HasShelvedGoals
-  else if not (CList.is_empty (p.given_up)) then
+  else if has_given_up_goals p then
     raise HasGivenUpGoals
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
@@ -311,6 +323,7 @@ let return p =
     Proofview.return p.proofview
 
 let initial_goals p = Proofview.initial_goals p.entry
+let initial_euctx p = p.initial_euctx
 
 let compact p =
   let entry, proofview = Proofview.compact p.entry p.proofview in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 2b85ec87..a0ed0654 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -69,11 +69,15 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre
 val start : Evd.evar_map -> (Environ.env * Term.types) list -> proof
 val dependent_start : Proofview.telescope -> proof
 val initial_goals : proof -> (Term.constr * Term.types) list
+val initial_euctx : proof -> Evd.evar_universe_context
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
     to be considered (this does not require that all evars have been solved). *)
 val is_done : proof -> bool
 
+(* Like is_done, but this time it really means done (i.e. nothing left to do) *)
+val is_complete : proof -> bool
+
 (* Returns the list of partial proofs to initial goals. *)
 val partial_proof : proof -> Term.constr list
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5bff3c81..c303f486 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -67,14 +67,14 @@ type proof_universes = Evd.evar_universe_context
 
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | 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
@@ -250,17 +250,43 @@ let start_dependent_proof id str goals terminator =
 
 let get_used_variables () = (cur_pstate ()).section_vars
 
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Proof using Clear Unused";
+      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
+      Goptions.optread  = (fun () -> !proof_using_auto_clear);
+      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
 let set_used_variables l =
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe, to_clear as orig) =
+    match entry with
+    | (x,None,_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+    | (x,Some bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+  let ctx, _, to_clear =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+  let to_clear = if !proof_using_auto_clear then to_clear else [] in
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
         Errors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
-      ctx
+      ctx, to_clear
 
 let get_open_goals () =
   let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
@@ -269,16 +295,14 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = 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
   let fpl, univs = Future.split2 fpl in
-  let universes = 
-    if poly || now then Future.force univs 
-    else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) 
-  in
-  (* Because of dependent subgoals at the begining of proofs, we could
+  let universes = if poly || now then Future.force univs else initial_euctx in
+  (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
@@ -289,19 +313,26 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
     if poly || now then
       let make_body t (c, eff) =
         let open Universes in
-	let body = c and typ = nf t in
+        let body = c in
+	let typ =
+	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
+	    nf t
+	  else t
+	in
         let used_univs_body = Universes.universes_of_constr body in
-	let used_univs_typ = Universes.universes_of_constr typ in
-	let ctx = Evd.evar_universe_context_set universes in
-        if keep_body_ucst_sepatate then
+        let used_univs_typ = Universes.universes_of_constr typ in
+        if keep_body_ucst_separate ||
+           not (Safe_typing.empty_private_constants = eff) then
+          let initunivs = Evd.evar_context_universe_context initial_euctx in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* 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 ctx_typ = restrict_universe_context ctx used_univs_typ in
-          let univs_typ = Univ.ContextSet.to_context ctx_typ in
-          (univs_typ, typ), ((body, ctx_body), eff)
+          (initunivs, typ), ((body, ctx_body), eff)
         else
+          let initunivs = Univ.UContext.empty in
+          let ctx = Evd.evar_universe_context_set initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
@@ -310,14 +341,13 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
           let univs = Univ.ContextSet.to_context ctx in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
-	fun t p ->
-	  Future.split2 (Future.chain ~pure:true p (make_body t))
+       fun t p -> Future.split2 (Future.chain ~pure:true p (make_body t))
     else
       fun t p ->
-        let initunivs = Evd.evar_context_universe_context universes in
-	  Future.from_val (initunivs, nf t), 
-	  Future.chain ~pure:true p (fun (pt,eff) ->
-	    (pt, Evd.evar_universe_context_set (Future.force univs)), eff)
+        let initunivs = Evd.evar_context_universe_context initial_euctx in
+        Future.from_val (initunivs, nf t),
+        Future.chain ~pure:true p (fun (pt,eff) ->
+          (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
@@ -336,15 +366,11 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
   { id = pid; entries = entries; persistence = strength; universes = universes },
   fun pr_ending -> Ephemeron.get terminator pr_ending
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_done proof then begin
-    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
-     str" is complete, no need to end it with Admitted");
-  end;
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
@@ -370,10 +396,7 @@ let return_proof ?(allow_partial=false) () =
     | Proof.HasUnresolvedEvar->
         error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd =
-    if poly || !Flags.compilation_mode = Flags.BuildVo
-    then Evd.nf_constraints evd
-    else evd in
+  let evd = Evd.nf_constraints evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
@@ -382,9 +405,9 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_sepatate fix_exn =
-  close_proof ~keep_body_ucst_sepatate ~now:true
+  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_separate fix_exn =
+  close_proof ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
@@ -668,4 +691,13 @@ let freeze ~marshallable =
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
-
+let copy_terminators ~src ~tgt =
+  assert(List.length src = List.length tgt);
+  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
+
+let update_global_env () =
+  with_current_proof (fun _ p ->
+     Proof.in_proof p (fun sigma ->
+       let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
+       let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
+         (p, ())))
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9d5038a3..a2254508 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -58,7 +58,7 @@ type lemma_possible_guards = int list list
 type proof_universes = Evd.evar_universe_context
 type proof_object = {
   id : Names.Id.t;
-  entries : Entries.definition_entry list;
+  entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
   universes: proof_universes;
   (* constraints : Univ.constraints; *)
@@ -66,7 +66,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | 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
@@ -89,15 +89,20 @@ val start_dependent_proof :
   Names.Id.t -> 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
+  there_are_pending_proofs. *)
+val update_global_env : unit -> unit
+
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
+val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The formes is supposed to be
+ * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
-type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
+type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 (* If allow_partial is set (default no) then an incomplete proof
  * is allowed (no error), and a warn is given if the proof is complete. *)
@@ -129,8 +134,10 @@ val set_interp_tac :
     -> unit
 
 (** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies *)
-val set_used_variables : Names.Id.t list -> Context.section_context
+ * (w.r.t. type dependencies and let-ins covered by it) + a list of
+ * ids to be cleared *)
+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
 
 (**********************************************************)
@@ -197,3 +204,4 @@ type state
 val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
 val proof_of_state : state -> Proof.proof
+val copy_terminators : src:state -> tgt:state -> state
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f66e9657..7eed1cb3 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -11,20 +11,15 @@ open Environ
 open Util
 open Vernacexpr
 
-let to_string = function
-  | SsAll -> "All"
-  | SsType -> "Type"
-  | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet [] -> "( )"
-        | SsSet [_,x] -> Id.to_string x
-        | SsSet l ->
-          "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")"
-        | SsCompl e -> "-" ^ aux e^""
-        | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
-        | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
-      in aux e
+let to_string e =
+  let rec aux = function
+    | SsEmpty -> "()"
+    | SsSingl (_,id) -> "("^Id.to_string id^")"
+    | SsCompl e -> "-" ^ aux e^""
+    | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+    | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+    | SsFwdClose e -> "("^aux e^")*"
+  in aux e
 
 let known_names = Summary.ref [] ~name:"proofusing-nameset"
 
@@ -36,30 +31,48 @@ let in_nameset =
     discharge_function = (fun _ -> None)
   }
 
+let rec close_fwd e s =
+  let s' =
+    List.fold_left (fun s (id,b,ty) ->      
+      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
+      let vty = global_vars_set e ty in
+      let vbty = Id.Set.union vb vty in
+      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
+      then Id.Set.add id (Id.Set.union s vbty) else s)
+    s (named_context e)
+    in
+  if Id.Set.equal s s' then s else close_fwd e s'
+;;
+
 let rec process_expr env e ty =
-  match e with
-  | SsAll ->
-      List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet l -> set_of_list env (List.map snd l)
-        | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
-        | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
-        | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-      in
-        aux e
-  | SsType ->
-      List.fold_left (fun acc ty ->
+  let rec aux = function
+    | SsEmpty -> Id.Set.empty
+    | SsSingl (_,id) -> set_of_id env ty id
+    | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
+    | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
+    | SsCompl e -> Id.Set.diff (full_set env) (aux e)
+    | SsFwdClose e -> close_fwd env (aux e)
+  in
+    aux e
+
+and set_of_id env ty id =
+  if Id.to_string id = "Type" then
+    List.fold_left (fun acc ty ->
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
-and set_of_list env = function
-  | [x] when CList.mem_assoc_f Id.equal x !known_names ->
-      process_expr env (CList.assoc_f Id.equal x !known_names) []
-  | l -> List.fold_right Id.Set.add l Id.Set.empty
-and full_set env = set_of_list env (List.map pi1 (named_context env))
+  else if Id.to_string id = "All" then
+    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  else if CList.mem_assoc_f Id.equal id !known_names then
+    process_expr env (CList.assoc_f Id.equal id !known_names) []
+  else Id.Set.singleton id
+
+and full_set env =
+  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
-  let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+  let v_ty = process_expr env ty_expr ty in
+  let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
@@ -77,62 +90,49 @@ let minimize_hyps env ids =
   in
     aux ids
 
-let minimize_unused_hyps env ids =
-  let all_ids = List.map pi1 (named_context env) in
-  let deps_of =
-    let cache =
-      List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in
-    fun id -> List.assoc id cache in
-  let inv_dep_of =
-    let cache_sum cache id stuff =
-      try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache
-      with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in
-    let cache =
-      List.fold_left (fun cache id ->
-        Id.Set.fold (fun d cache -> cache_sum cache d id)
-          (Id.Set.remove id (deps_of id)) cache)
-        Id.Map.empty all_ids in
-    fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in
-  let rec aux s =
-    let s' =
-      Id.Set.fold (fun id s ->
-        if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id)
-        else s)
-      s s in
-    if Id.Set.equal s s' then s else aux s' in
-  aux ids
-
-let suggest_Proof_using kn env vars ids_typ context_ids =
+let remove_ids_and_lets env s ids =
+  let not_ids id = not (Id.Set.mem id ids) in
+  let no_body id = named_body id env = None in
+  let deps id = really_needed env (Id.Set.singleton id) in
+    (Id.Set.filter (fun id ->
+      not_ids id &&
+     (no_body id ||
+       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
+
+let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env used in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let unneeded = minimize_unused_hyps env (S.diff all needed) in
-  let pr_set s =
+  let print x = prerr_endline (string_of_ppcmds x) in
+  let pr_set parens s =
     let wrap ppcmds =
-      if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
-      then str "(" ++ ppcmds ++ str ")"
+      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
       else ppcmds in
     wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
+  let used = S.union vars ids_typ in
+  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
+  let all_needed = really_needed env needed in
+  let all = List.fold_right S.add context_ids S.empty in
+  let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
-    prerr_endline (string_of_ppcmds (str "All " ++ pr_set all));
-    prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ));
-    prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed));
-    prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded));
+    print (str "All "        ++ pr_set false all);
+    print (str "Type "       ++ pr_set false ids_typ);
+    print (str "needed "     ++ pr_set false needed);
+    print (str "all_needed " ++ pr_set false all_needed);
+    print (str "Type* "      ++ pr_set false fwd_typ);
   end;
+  let valid_exprs = ref [] in
+  let valid e = valid_exprs := e :: !valid_exprs in
+  if S.is_empty needed then valid (str "Type");
+  if S.equal all_needed fwd_typ then valid (str "Type*");
+  if S.equal all all_needed then valid(str "All");
+  valid (pr_set false needed);
   msg_info (
-    str"The proof of "++
-    Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++
-    str"Proof using " ++
-    if S.is_empty needed then str "."
-    else if S.subset needed ids_typ then str "Type."
-    else if S.equal all all_needed then str "All."
-    else 
-      let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in
-      let s2 = string_of_ppcmds (pr_set needed ++ str".") in
-      if String.length s1 < String.length s2 then str s1 else str s2)
+    str"The proof of "++ str name ++ spc() ++
+    str "should start with one of the following commands:"++spc()++
+    v 0 (
+    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
+  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
+;;
 
 let value = ref false
 
@@ -146,13 +146,13 @@ let _ =
       Goptions.optwrite = (fun b ->
         value := b;
         if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ())
+        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
       ) }
 
-let value = ref "_unset_"
+let value = ref None
 
 let _ =
-  Goptions.declare_string_option
+  Goptions.declare_stringopt_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
@@ -161,6 +161,4 @@ let _ =
       Goptions.optwrite = (fun b -> value := b;) }
 
 
-let get_default_proof_using () =
-  if !value = "_unset_" then None
-  else Some !value
+let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index fb3497f1..dcf8a0fc 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,21 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and [keep_hyps e s1] is equal to [keep_hyps e s2].  Inefficient. *)
-val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
-(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and s.t. calling [clear s1] would do the same as [clear s2].  Inefficient. *)
-val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
 val process_expr :
-  Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
+  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
     Names.Id.t list
 
-val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
-val to_string : Vernacexpr.section_subset_descr -> string
+val to_string : Vernacexpr.section_subset_expr -> string
 
 val get_default_proof_using : unit -> string option
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6f626341..4fc0c164 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -384,20 +384,23 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
 let tclFOCUSID id t =
   let open Proof in
   Pv.get >>= fun initial ->
-  let rec aux n = function
-    | [] -> tclZERO (NoSuchGoals 1)
-    | g::l ->
-        if Names.Id.equal (Evd.evar_ident g initial.solution) id then
-          let (focused,context) = focus n n initial in
-          Pv.set focused >>
-          t >>= fun result ->
-          Pv.modify (fun next -> unfocus context next) >>
-          return result
-        else
-          aux (n+1) l in
-  aux 1 initial.comb
-
-
+  try
+    let ev = Evd.evar_key id initial.solution in
+    try
+      let n = CList.index Evar.equal ev initial.comb in
+      (* goal is already under focus *)
+      let (focused,context) = focus n n initial in
+      Pv.set focused >>
+        t >>= fun result ->
+      Pv.modify (fun next -> unfocus context next) >>
+        return result
+    with Not_found ->
+      (* otherwise, save current focus and work purely on the shelve *)
+      Comb.set [ev] >>
+        t >>= fun result ->
+      Comb.set initial.comb  >>
+        return result
+  with Not_found -> tclZERO (NoSuchGoals 1)
 
 (** {7 Dispatching on goals} *)
 
@@ -648,7 +651,7 @@ let goodmod p m =
 
 let cycle n =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let n' = goodmod n l in
@@ -658,7 +661,7 @@ let cycle n =
 
 let swap i j =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -722,19 +725,7 @@ let give_up =
 
 module Progress = struct
 
-  (** equality function up to evar instantiation in heterogeneous
-      contexts. *)
-  (* spiwack (2015-02-19): In the previous version of progress an
-     equality which considers two universes equal when it is consistent
-     tu unify them ([Evd.eq_constr_univs_test]) was used. Maybe this
-     behaviour has to be restored as well. This has to be established by
-     practice. *)
-    
-  let rec eq_constr sigma1 sigma2 t1 t2 =
-    Constr.equal_with
-      (fun t -> Evarutil.kind_of_term_upto sigma1 t)
-      (fun t -> Evarutil.kind_of_term_upto sigma2 t)
-      t1 t2
+  let eq_constr = Evarutil.eq_constr_univs_test
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -1069,7 +1060,7 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.set { solution = sigma; comb; }
   end
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5a9e7f39..927df33a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -336,7 +336,7 @@ val tclENV : Environ.env tactic
 (** {7 Put-like primitives} *)
 
 (** [tclEFFECTS eff] add the effects [eff] to the current state. *)
-val tclEFFECTS : Declareops.side_effects -> unit tactic
+val tclEFFECTS : Safe_typing.private_constants -> unit tactic
 
 (** [mark_as_unsafe] declares the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1383d755..be92f2b0 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -30,9 +30,12 @@ let cbv_vm env sigma c =
   Vnorm.cbv_vm env c ctyp
 
 let cbv_native env sigma c =
-  let ctyp = Retyping.get_type_of env sigma c in
-  let evars = Nativenorm.evars_of_evar_map sigma in
-  Nativenorm.native_norm env evars c ctyp
+  if Coq_config.no_native_compiler then
+    let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
+    cbv_vm env sigma c
+  else
+    let ctyp = Retyping.get_type_of env sigma c in
+    Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
@@ -167,18 +170,20 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.declare_reduction"
+    (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then error ("Reference to undefined reduction expression "^s)
+      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then error ("There is already a reduction expression of name "^s)
+  then errorlabstrm "Redexpr.decl_red_expr"
+    (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
     red_expr_tab := String.Map.add s e !red_expr_tab
@@ -232,7 +237,8 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   error("unknown user-defined reduction \""^s^"\"")))
+	   errorlabstrm "Redexpr.reduction_of_red_expr"
+             (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 974fa212..ba62b2cb 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -186,10 +186,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
-(* Execute tac and show the names of hypothesis create by tac in
-   the "as" format. The resulting goals are printed *after* the
-   as-expression, which forces pg to some gymnastic. TODO: Have
-   something similar (better?) in the xml protocol. *)
+(* Execute tac, show the names of new hypothesis names created by tac
+   in the "as" format and then forget everything. From the logical
+   point of view [tclSHOWHYPS tac] is therefore equivalent to idtac,
+   except that it takes the time and memory of tac and prints "as"
+   information). The resulting (unchanged) goals are printed *after*
+   the as-expression, which forces pg to some gymnastic.
+   TODO: Have something similar (better?) in the xml protocol.
+   NOTE: some tactics delete hypothesis and reuse names (induction,
+   destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
   let oldhyps:Context.named_context = pf_hyps goal in
@@ -197,9 +202,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   let { it = gls; sigma = sigma; } = rslt in
   let hyps:Context.named_context list =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
+  let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in
   let newhyps =
     List.map
-      (fun hypl -> List.subtract Context.eq_named_declaration hypl oldhyps)
+      (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
   let emacs_str s =
@@ -215,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   pp (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
       ++  (str (emacs_str "</infoH>")) ++ fnl());
-  rslt;;
+  tclIDTAC goal;;
 
 
 let catch_failerror (e, info) =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fa0d0362..4238d1e3 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -84,6 +84,7 @@ let pf_nf                        = pf_reduce simpl
 let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+let pf_unsafe_type_of            = pf_reduce unsafe_type_of
 let pf_type_of                   = pf_reduce type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
@@ -172,6 +173,9 @@ module New = struct
   let pf_env = Proofview.Goal.env
   let pf_concl = Proofview.Goal.concl
 
+  let pf_unsafe_type_of gl t =
+    pf_apply unsafe_type_of gl t
+
   let pf_type_of gl t =
     pf_apply type_of gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f7fc6b54..a0e1a015 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,7 +41,8 @@ val pf_nth_hyp_id         : goal sigma -> int -> Id.t
 val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
-val pf_type_of            : goal sigma -> constr -> types
+val pf_unsafe_type_of            : goal sigma -> constr -> types
+val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
@@ -112,7 +113,8 @@ module New : sig
   val pf_env : 'a Proofview.Goal.t -> Environ.env
   val pf_concl : [ `NF ] Proofview.Goal.t -> types
 
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
   val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
   val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 3cc81daf..6d6215c5 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -11,6 +11,7 @@ open Names
 open Pp
 open Tacexpr
 open Termops
+open Nameops
 
 let (prtac, tactic_printer) = Hook.make ()
 let (prmatchpatt, match_pattern_printer) = Hook.make ()
@@ -31,7 +32,8 @@ let explain_logic_error = ref (fun e -> mt())
 
 let explain_logic_error_no_anomaly = ref (fun e -> mt())
 
-let msg_tac_debug s = Proofview.NonLogical.print (s++fnl())
+let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl())
+let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
 
 (* Prints the goal *)
 
@@ -47,7 +49,7 @@ let db_pr_goal gl =
 let db_pr_goal =
   Proofview.Goal.nf_enter begin fun gl ->
   let pg = db_pr_goal gl in
-  Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
+  Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
   end
 
 
@@ -120,7 +122,7 @@ let run ini =
   let open Proofview.NonLogical in
   if not ini then
     begin
-      Proofview.NonLogical.print (str"\b\r\b\r") >>
+      Proofview.NonLogical.print_notice (str"\b\r\b\r") >>
       !skipped >>= fun skipped ->
       msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl())
     end >>
@@ -135,7 +137,7 @@ let rec prompt level =
   let runtrue = run true in
   begin
     let open Proofview.NonLogical in
-    Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+    Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
     let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
     Proofview.NonLogical.catch Proofview.NonLogical.read_line
       begin function (e, info) -> match e with
@@ -231,17 +233,16 @@ let db_pattern_rule debug num r =
 
 (* Prints the hypothesis pattern identifier if it exists *)
 let hyp_bound = function
-  | Anonymous -> " (unbound)"
-  | Name id -> " (bound to "^(Names.Id.to_string id)^")"
+  | Anonymous -> str " (unbound)"
+  | Name id -> str " (bound to " ++ pr_id id ++ str ")"
 
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,_,c) ido =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Hypothesis " ++
-           str ((Names.Id.to_string id)^(hyp_bound ido)^
-                " has been matched: ") ++ print_constr_env env c)
+    msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+                str " has been matched: " ++ print_constr_env env c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -266,8 +267,8 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
-                " cannot match: ") ++
+    msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
+                str " cannot match: " ++
            Hook.get prmatchpatt env sigma hyp)
   else return ()