Merge branch 'v8.5'

26 files changed, 286 insertions, 221 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 650897ef74..f969f01329 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -502,7 +502,7 @@ open Egramml
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
@@ -519,7 +519,7 @@ let _ =
 
 let _ =
   try
-    Vernacinterp.vinterp_add ("PrintPureConstr", 0)
+    Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
          [c] when genarg_tag c = ConstrArgType && true ->
            let c = out_gen (rawwit wit_constr) c in
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 7a4d52ab81..9db89308fb 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -17,6 +17,19 @@ open Pcoq
 open Egramml
 open Compat
 
+type rule = {
+  r_head : string option;
+  (** The first terminal grammar token *)
+  r_patt : grammar_prod_item list;
+  (** The remaining tokens of the parsing rule *)
+  r_class : MLast.expr option;
+  (** An optional classifier for the STM *)
+  r_branch : MLast.expr;
+  (** The action performed by this rule. *)
+  r_depr : unit option;
+  (** Whether this entry is deprecated *)
+}
+
 let rec make_let e = function
   | [] -> e
   | GramNonTerminal(loc,t,_,Some p)::l ->
@@ -27,7 +40,7 @@ let rec make_let e = function
       <:expr< let $lid:p$ = Genarg.out_gen $make_rawwit loc t$ $lid:p$ in $e$ >>
   | _::l -> make_let e l
 
-let make_clause (_,pt,_,e) =
+let make_clause { r_patt = pt; r_branch = e; } =
   (make_patt pt,
    vala (Some (make_when (MLast.loc_of_expr e) pt)),
    make_let e pt)
@@ -41,7 +54,7 @@ let mk_ignore c pt =
   let names = List.fold_left fold <:expr< () >> names in
   <:expr< do { let _ = $names$ in $c$ } >>
 
-let make_clause_classifier cg s (_,pt,c,_) =
+let make_clause_classifier cg s { r_patt = pt; r_class = c; } =
   match c ,cg with
   | Some c, _ ->
      (make_patt pt,
@@ -76,8 +89,15 @@ let make_clause_classifier cg s (_,pt,c,_) =
       <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>)
 
 let make_fun_clauses loc s l =
-  let cl = List.map (fun c -> Compat.make_fun loc [make_clause c]) l in
-  mlexpr_of_list (fun x -> x) cl
+  let map c =
+    let depr = match c.r_depr with
+    | None -> false
+    | Some () -> true
+    in
+    let cl = Compat.make_fun loc [make_clause c] in
+    <:expr< ($mlexpr_of_bool depr$, $cl$)>>
+  in
+  mlexpr_of_list map l
 
 let make_fun_classifiers loc s c l =
   let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in
@@ -85,7 +105,7 @@ let make_fun_classifiers loc s c l =
 
 let mlexpr_of_clause =
   mlexpr_of_list
-    (fun (a,b,_,_) -> mlexpr_of_list make_prod_item
+    (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item
        (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b))
 
 let declare_command loc s c nt cl =
@@ -96,7 +116,7 @@ let declare_command loc s c nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try do {
-          CList.iteri (fun i f -> Vernacinterp.vinterp_add ($se$, i) f) $funcl$;
+          CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$;
           CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ }
 	with [ e when Errors.noncritical e ->
 	  Pp.msg_warning
@@ -135,22 +155,28 @@ EXTEND
           <:expr< fun _ -> Vernac_classifier.classify_as_query >>
     ] ]
   ;
+  deprecation:
+    [ [ "DEPRECATED" -> () ] ]
+  ;
   (* spiwack: comment-by-guessing: it seems that the isolated string (which
       otherwise could have been another argument) is not passed to the
       VernacExtend interpreter function to discriminate between the clauses. *)
   rule:
     [ [ "["; s = STRING; l = LIST0 args; "]";
-        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ];
-                  "->"; "["; e = Pcaml.expr; "]" ->
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
       if String.is_empty s then
         Errors.user_err_loc (!@loc,"",Pp.str"Command name is empty.");
-      (Some s,l,c,<:expr< fun () -> $e$ >>)
+      let b = <:expr< fun () -> $e$ >> in
+      { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
       | "[" ; "-" ; l = LIST1 args ; "]" ;
-        c = OPT [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ];
-                  "->"; "["; e = Pcaml.expr; "]" ->
-      (None,l,c,<:expr< fun () -> $e$ >>)
+        d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" ->
+      let b = <:expr< fun () -> $e$ >> in
+      { r_head = None; r_patt = l; r_class = c; r_branch = b; r_depr = d; }
     ] ]
   ;
+  classifier:
+    [ [ "=>"; "["; c = Pcaml.expr; "]" -> <:expr< fun () -> $c$>> ] ]
+  ;
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let t, g = interp_entry_name false None e "" in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 4564d620ea..c977879a7b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -855,8 +855,10 @@ let refresh_editor_prefs () =
     Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color);
     sn.script#misc#modify_base [`NORMAL, `COLOR clr];
     sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
-    sn.command#refresh_color ()
+    sn.messages#refresh_color ();
+    sn.command#refresh_color ();
+    sn.errpage#refresh_color ();
+    sn.jobpage#refresh_color ();
 
   in
   List.iter iter_session notebook#pages
diff --git a/ide/session.ml b/ide/session.ml
index dc79fa7905..e0466b7e3a 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -18,6 +18,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
@@ -256,6 +257,10 @@ let make_table_widget cd cb =
       ~rules_hint:true ~headers_visible:false
       ~model:store ~packing:frame#add () in
   let () = data#set_headers_visible true in
+  let refresh () =
+    let clr = Tags.color_of_string current.background_color in
+    data#misc#modify_base [`NORMAL, `COLOR clr]
+  in
   let mk_rend c = GTree.cell_renderer_text [], ["text",c] in
   let cols =
     List.map2 (fun (_,c) (_,n,v) ->
@@ -271,10 +276,10 @@ let make_table_widget cd cb =
   ignore(
     data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc)
   );
-  frame, (fun f -> f columns store)
+  frame, (fun f -> f columns store), refresh
 
 let create_errpage (script : Wg_ScriptView.script_view) : errpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`Int,"Line",true; `String,"Error message",true]
       (fun columns store tp vc ->
@@ -305,10 +310,11 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_jobpage coqtop coqops : jobpage =
-  let table, access =
+  let table, access, refresh =
     make_table_widget
       [`String,"Worker",true; `String,"Job name",true]
       (fun columns store tp vc ->
@@ -344,6 +350,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method refresh_color () = refresh ()
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 3a6b458582..52e5572186 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method refresh_color : unit -> unit
   end
 
 class type control =
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index b32674084d..211db537ed 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -33,6 +33,7 @@ class type message_view =
     method buffer : GText.buffer
       (** for more advanced text edition *)
     method modify_font : Pango.font_description -> unit
+    method refresh_color : unit -> unit
   end
 
 let message_view () : message_view =
@@ -83,4 +84,9 @@ let message_view () : message_view =
 
     method modify_font fd = view#misc#modify_font fd
 
+    method refresh_color () =
+      let open Preferences in
+      let clr = Tags.color_of_string current.background_color in
+      view#misc#modify_base [`NORMAL, `COLOR clr]
+
   end
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 4dcd7306ba..23c94f4048 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -25,6 +25,7 @@ class type message_view =
     method buffer : GText.buffer
       (** for more advanced text edition *)
     method modify_font : Pango.font_description -> unit
+    method refresh_color : unit -> unit
   end
 
 val message_view : unit -> message_view
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 58e1eb1d17..f57772ecb0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -977,7 +977,7 @@ let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
   | PVar id -> GVar (loc,id)
   | PEvar (evk,l) ->
-      let test id = function PVar id' -> Id.equal id id' | _ -> false in
+      let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
       let id = Evd.evar_ident evk sigma in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 20cecc84a6..65d1de7e11 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -379,7 +379,9 @@ let globalize_constant_universes env cb =
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later (Future.chain ~pure:true fc Univ.ContextSet.constraints)]
+            | None -> [Later (Future.chain
+                 ~greedy:(not (Future.is_exn fc))
+                 ~pure:true fc Univ.ContextSet.constraints)]
             | Some c -> [Now (Univ.ContextSet.constraints c)])
       
 let globalize_mind_universes mb =
diff --git a/lib/future.ml b/lib/future.ml
index 2f1ce5e4e9..02d3702d77 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -11,19 +11,21 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t)
 let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
 let set_freeze f g = freeze := f; unfreeze := g
 
-exception NotReady
-exception NotHere
+exception NotReady of string
+exception NotHere of string
 let _ = Errors.register_handler (function
-  | NotReady ->
-      Pp.strbrk("The value you are asking for is not ready yet. " ^
+  | NotReady name ->
+      Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing.")
-  | NotHere ->
-      Pp.strbrk("The value you are asking for is not available "^
+                "asynchronous script processing and don't pass \"-quick\" to "^
+                "coqc.")
+  | NotHere name ->
+      Pp.strbrk("The value you are asking for ("^name^") is not available "^
                 "in this process. If you really need this, pass "^
                 "the \"-async-proofs off\" option to CoqIDE to disable "^
-                "asynchronous script processing.")
+                "asynchronous script processing and don't pass \"-quick\" to "^
+                "coqc.")
   | _ -> raise Errors.Unhandled)
 
 type fix_exn = Exninfo.iexn -> Exninfo.iexn
@@ -54,67 +56,69 @@ and 'a comp =
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
-  | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
+  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
   | Finished of 'a
 
 and 'a computation = 'a comput ref
 
-let create ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (Ephemeron.create (uuid, f, Pervasives.ref x)))
+let unnamed = "unnamed"
+
+let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
+  ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
-  | Finished v -> UUID.invalid, id, ref (Val (v,None))
-  | Ongoing x ->
-      try Ephemeron.get x
+  | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
+  | Ongoing (name, x) ->
+      try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c
       with Ephemeron.InvalidKey ->
-        UUID.invalid, id, ref (Exn (NotHere, Exninfo.null))
+        name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))
 
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
 
-let is_over kx = let _, _, x = get kx in match !x with
+let is_over kx = let _, _, _, x = get kx in match !x with
   | Val _ | Exn _ -> true
   | Closure _ | Delegated _ -> false
 
-let is_val kx = let _, _, x = get kx in match !x with
+let is_val kx = let _, _, _, x = get kx in match !x with
   | Val _ -> true
   | Exn _ | Closure _ | Delegated _ -> false
 
-let is_exn kx = let _, _, x = get kx in match !x with
+let is_exn kx = let _, _, _, x = get kx in match !x with
   | Exn _ -> true
   | Val _ | Closure _ | Delegated _ -> false
 
-let peek_val kx = let _, _, x = get kx in match !x with
+let peek_val kx = let _, _, _, x = get kx in match !x with
   | Val (v, _) -> Some v
   | Exn _ | Closure _ | Delegated _ -> None
 
-let uuid kx = let id, _, _ = get kx in id
+let uuid kx = let _, id, _, _ = get kx in id
 
 let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
 let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
-let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
+let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
-let create_delegate ?(blocking=true) fix_exn =
+let create_delegate ?(blocking=true) ~name fix_exn =
   let assignement signal ck = fun v ->
-    let _, fix_exn, c = get ck in
+    let _, _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
     begin match v with
     | `Val v -> c := Val (v, None)
     | `Exn e -> c := Exn (fix_exn e)
-    | `Comp f -> let _, _, comp = get f in c := !comp end;
+    | `Comp f -> let _, _, _, comp = get f in c := !comp end;
     signal () in
   let wait, signal =
-    if not blocking then (fun () -> raise NotReady), ignore else
+    if not blocking then (fun () -> raise (NotReady name)), ignore else
     let lock = Mutex.create () in
     let cond = Condition.create () in
     (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
     (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
-  let ck = create fix_exn (Delegated wait) in
+  let ck = create ~name fix_exn (Delegated wait) in
   ck, assignement signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
 let rec compute ~pure ck : 'a value =
-  let _, fix_exn, c = get ck in
+  let _, _, fix_exn, c = get ck in
   match !c with
   | Val (x, _) -> `Val x
   | Exn (e, info) -> `Exn (e, info)
@@ -128,7 +132,7 @@ let rec compute ~pure ck : 'a value =
         let e = Errors.push e in
         let e = fix_exn e in
         match e with
-        | (NotReady, _) -> `Exn e
+        | (NotReady _, _) -> `Exn e
         | _ -> c := Exn e; `Exn e
 
 let force ~pure x = match compute ~pure x with
@@ -136,8 +140,8 @@ let force ~pure x = match compute ~pure x with
   | `Exn e -> Exninfo.iraise e
 
 let chain ~pure ck f =
-  let uuid, fix_exn, c = get ck in
-  create ~uuid fix_exn (match !c with
+  let name, uuid, fix_exn, c = get ck in
+  create ~uuid ~name fix_exn (match !c with
   | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
   | Exn _ as x -> x
   | Val (v, None) when pure -> Closure (fun () -> f v)
@@ -156,7 +160,7 @@ let chain ~pure ck f =
 let create fix_exn f = create fix_exn (Closure f)
 
 let replace kx y =
-  let _, _, x = get kx in
+  let _, _, _, x = get kx in
   match !x with
   | Exn _ -> x := Closure (fun () -> force ~pure:false y)
   | _ -> Errors.anomaly
@@ -207,10 +211,10 @@ let map2 ?greedy f x l =
 
 let print f kx =
   let open Pp in
-  let (uid, _, x) = get kx in
+  let name, uid, _, x = get kx in
   let uid =
-    if UUID.equal uid UUID.invalid then str "[#]"
-    else str "[" ++ int uid ++ str "]"
+    if UUID.equal uid UUID.invalid then str "[#:" ++ str name ++ str "]"
+    else str "[" ++ int uid ++ str":" ++ str name ++ str "]"
   in
   match !x with
   | Delegated _ -> str "Delegated" ++ uid
diff --git a/lib/future.mli b/lib/future.mli
index 8a4fa0bdfb..324d5f7d10 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -63,7 +63,7 @@ end
 module UUIDMap : Map.S with type key = UUID.t
 module UUIDSet : Set.S with type elt = UUID.t
 
-exception NotReady
+exception NotReady of string
 
 type 'a computation
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ]
@@ -100,7 +100,8 @@ val fix_exn_of : 'a computation -> fix_exn
    delage assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
-  ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit)
+  ?blocking:bool -> name:string ->
+  fix_exn -> 'a computation * ('a assignement -> unit)
 
 (* Given a computation that is_exn, replace it by another one *)
 val replace : 'a computation -> 'a computation -> unit
diff --git a/library/assumptions.ml b/library/assumptions.ml
index ab07b3647e..62645b2365 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -21,6 +21,7 @@ open Names
 open Term
 open Declarations
 open Mod_subst
+open Globnames
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -158,94 +159,67 @@ let lookup_constant cst =
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
-let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) =
-  modcache := MPmap.empty;
-  let (idts,knst) = st in
-  (* Infix definition for chaining function that accumulate
-     on a and a ContextObjectSet, ContextObjectMap.  *)
-  let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
-  (* This function eases memoization, by checking if an object is already
-     stored before trying and applying a function.
-     If the object is there, the function is not fired (we are in a
-     particular case where memoized object don't need a treatment at all).
-     If the object isn't there, it is stored and the function is fired*)
-  let try_and_go o f s m =
-    if ContextObjectSet.mem o s then
-      (s,m)
-    else
-      f (ContextObjectSet.add o s) m
-  in
-  let identity2 s m = (s,m)
+(** Graph traversal of an object, collecting on the way the dependencies of
+    traversed objects *)
+let rec traverse accu t = match kind_of_term t with
+| Var id ->
+  let body () = match Global.lookup_named id with (_, body, _) -> body in
+  traverse_object accu body (VarRef id)
+| Const (kn, _) ->
+  let body () = Global.body_of_constant_body (lookup_constant kn) in
+  traverse_object accu body (ConstRef kn)
+| Ind (ind, _) ->
+  traverse_object accu (fun () -> None) (IndRef ind)
+| Construct (cst, _) ->
+  traverse_object accu (fun () -> None) (ConstructRef cst)
+| Meta _ | Evar _ -> assert false
+| _ -> Constr.fold traverse accu t
+
+and traverse_object (curr, data) body obj =
+  let data =
+    if Refmap.mem obj data then data
+    else match body () with
+    | None -> Refmap.add obj Refset.empty data
+    | Some body ->
+      let (contents, data) = traverse (Refset.empty, data) body in
+      Refmap.add obj contents data
   in
-  (* Goes recursively into the term to see if it depends on assumptions.
-    The 3 important cases are :
-     - Const _ where we need to first unfold the constant and return
-       the needed assumptions of its body in the environment,
-     - Rel _ which means the term is a variable which has been bound
-       earlier by a Lambda or a Prod (returns [] ),
-     - Var _ which means that the term refers to a section variable or
-       a "Let" definition, in the former it is an assumption of [t],
-       in the latter is must be unfolded like a Const.
-    The other cases are straightforward recursion.
-    Calls to the environment are memoized, thus avoiding exploration of
-    the DAG of the environment as if it was a tree (can cause
-    exponential behavior and prevent the algorithm from terminating
-    in reasonable time). [s] is a set of [context_object], representing
-    the object already visited.*)
-  let rec do_constr t s acc =
-    let rec iter t =
-      match kind_of_term t with
-	| Var id -> do_memoize_id id
-	| Meta _ | Evar _ -> assert false
-	| Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) ->
-	  (iter e1)**(iter e2)
-	| LetIn (_,e1,e2,e3) -> (iter e1)**(iter e2)**(iter e3)
-	| App (e1, e_array) -> (iter e1)**(iter_array e_array)
-	| Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array)
-	| Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) ->
-          (iter_array e1_array) ** (iter_array e2_array)
-	| Const (kn,_) -> do_memoize_kn kn
-	| Proj (_, e) -> iter e
-	| Rel _ | Sort _ | Ind _ | Construct _ -> identity2
-    and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2
-    in iter t s acc
-
-  and add_id id s acc =
-    (* a Var can be either a variable, or a "Let" definition.*)
-    match Global.lookup_named id with
-    | (_,None,t) ->
-        (s,ContextObjectMap.add (Variable id) t acc)
-    | (_,Some bdy,_) -> do_constr bdy s acc
-
-  and do_memoize_id id =
-    try_and_go (Variable id) (add_id id)
-
-  and add_kn kn s acc =
+  (Refset.add obj curr, data)
+
+let traverse t =
+  let () = modcache := MPmap.empty in
+  traverse (Refset.empty, Refmap.empty) t
+
+(** Hopefully bullet-proof function to recover the type of a constant. It just
+    ignores all the universe stuff. There are many issues that can arise when
+    considering terms out of any valid environment, so use with caution. *)
+let type_of_constant cb = match cb.Declarations.const_type with
+| Declarations.RegularArity ty -> ty
+| Declarations.TemplateArity (ctx, arity) ->
+  Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level)
+
+let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
+  let (idts, knst) = st in
+  (** Only keep the transitive dependencies *)
+  let (_, graph) = traverse t in
+  let fold obj _ accu = match obj with
+  | VarRef id ->
+    let (_, body, t) = Global.lookup_named id in
+    if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
+    else accu
+  | ConstRef kn ->
     let cb = lookup_constant kn in
-    let do_type cst =
-      let ctype = Global.type_of_global_unsafe (Globnames.ConstRef kn) in
-	(s,ContextObjectMap.add cst ctype acc)
-    in
-    let (s,acc) =
-      if Declareops.constant_has_body cb then
-        if Declareops.is_opaque cb || not (Cpred.mem kn knst) then
-          (** it is opaque *)
-          if add_opaque then do_type (Opaque kn)
-          else (s, acc)
-        else
-          if add_transparent then do_type (Transparent kn)
-          else (s, acc)
-      else (s, acc)
-    in
-      match Global.body_of_constant_body cb with
-      | None -> do_type (Axiom kn)
-      | Some body -> do_constr body s acc
-
-  and do_memoize_kn kn =
-    try_and_go (Axiom kn) (add_kn kn)
-
- in
- fun t ->
-   snd (do_constr t
-	  (ContextObjectSet.empty)
-	  (ContextObjectMap.empty))
+    if not (Declareops.constant_has_body cb) then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Axiom kn) t accu
+    else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Opaque kn) t accu
+    else if add_transparent then
+      let t = type_of_constant cb in
+      ContextObjectMap.add (Transparent kn) t accu
+    else
+      accu
+  | IndRef _ | ConstructRef _ -> accu
+  in
+  Refmap.fold fold graph ContextObjectMap.empty
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 0a2c62f582..809e536b43 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Term
+open Globnames
 
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
@@ -23,8 +24,18 @@ module ContextObjectSet : Set.S with type elt = context_object
 module ContextObjectMap : Map.ExtS
   with type key = context_object and module Set := ContextObjectSet
 
-(** collects all the assumptions (optionally including opaque definitions)
-   on which a term relies (together with their type) *)
+(** Collects all the objects on which a term directly relies, bypassing kernel
+    opacity, together with the recursive dependence DAG of objects.
+
+    WARNING: some terms may not make sense in the environement, because they are
+    sealed inside opaque modules. Do not try to do anything fancy with those
+    terms apart from printing them, otherwise demons may fly out of your nose.
+*)
+val traverse : constr -> (Refset.t * Refset.t Refmap.t)
+
+(** Collects all the assumptions (optionally including opaque definitions)
+   on which a term relies (together with their type). The above warning of
+   {!traverse} also applies. *)
 val assumptions :
   ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> constr ->
     Term.types ContextObjectMap.t
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 046ee0dad5..28fb8cbe36 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t =
 	  else noparams ()
 
     | Evar (evk,cl) ->
-        let bound_to_itself id c =
+        let bound_to_itself_or_letin (id,b,_) c =
+          b != None ||
 	  try let n = List.index Name.equal (Name id) (fst env) in 
-	      isRelN n c 
+	      isRelN n c
 	  with Not_found -> isVarId id c in
       let id,l =
         try
           let id = Evd.evar_ident evk sigma in
-          let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in
-          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in
-          let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
+          let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
+          let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
+          let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
           id,l
         with Not_found ->
           Id.of_string ("X" ^ string_of_int (Evar.repr evk)), 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index adfe9dd8de..b01f29a40a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -217,7 +217,7 @@ let compute_var_aliases sign =
     sign Id.Map.empty
 
 let compute_rel_aliases var_aliases rels =
-  snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+  snd (List.fold_right (fun (_,b,u) (n,aliases) ->
     (n-1,
      match b with
      | Some t ->
@@ -231,7 +231,7 @@ let compute_rel_aliases var_aliases rels =
                try Int.Map.find (p+n) aliases with Not_found -> [] in
              Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
          | _ ->
-             Int.Map.add n [lift n t] aliases)
+             Int.Map.add n [lift n (mkCast(t,DEFAULTcast,u))] aliases)
      | None -> aliases))
          rels (List.length rels,Int.Map.empty))
 
@@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
+let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct ((ind,_),u) ->
@@ -1025,44 +1025,31 @@ let rec is_constrainable_in top k (ev,(fv_rels,fv_ids) as g) t =
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false k g) args
-  | Prod (_,t1,t2) -> is_constrainable_in false k g t1 && is_constrainable_in false k g t2
-  | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+      Array.for_all (is_constrainable_in false force k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false force k g) args
+  | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2
+  | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
 
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
+let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
-  | _ -> is_constrainable_in true k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
-  let filter1 =
-    restrict_upon_filter evd evk1 (noccur_evar env evd evk2) argsv1
-  in
-  let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
-  let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
-  let filter2 =
-    restrict_upon_filter evd evk2 (noccur_evar env evd evk1) argsv2
-  in
-  let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
-  let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
-  evd,ev1,ev2
+  | _ -> is_constrainable_in true force k (ev,fvs) t
 
 exception EvarSolvedOnTheFly of evar_map * constr
 
 (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on
    the common domain of definition *)
-let project_evar_on_evar g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
   (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
   let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
   let filter1 = restrict_upon_filter evd evk1
-    (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+    (has_constrainable_free_vars evd aliases force k2 evk2 fvs2)
     argsv1 in
   let candidates1 =
     try restrict_candidates g env evd filter1 ev1 ev2
@@ -1098,9 +1085,9 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
-let solve_evar_evar_l2r f g env evd aliases pbty ev1 (evk2,_ as ev2) =
+let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
-    let evd,body = project_evar_on_evar g env evd aliases 0 pbty ev1 ev2 in
+    let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
@@ -1117,27 +1104,23 @@ let preferred_orientation evd evk1 evk2 =
   | _,Evar_kinds.QuestionMark _ -> false
   | _ -> true
 
-let solve_evar_evar_aux f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env in
   if preferred_orientation evd evk1 evk2 then
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
     add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
   else
-    try solve_evar_evar_l2r f g env evd aliases pbty ev1 ev2
+    try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2
     with CannotProject (evd,ev1) ->
-    try solve_evar_evar_l2r f g env evd aliases (opp_problem pbty) ev2 ev1
+    try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1
     with CannotProject (evd,ev2) ->
     add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd
 
-let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
-  let (evd,(evk1,args1 as ev1),(evk2,args2 as ev2)),pbty =
-    (* If an evar occurs in the instance of the other evar and the
-       use of an heuristic is forced, we restrict *)
-    if force then ensure_evar_independent g env evd ev1 ev2, None
-    else (evd,ev1,ev2),pbty in
+let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
+  let pbty = if force then None else pbty in
   let evi = Evd.find evd evk1 in
   let evd =
     try 
@@ -1166,7 +1149,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty ev1 ev2 =
           downcast evk2 t2 (downcast evk1 t1 evd)
     with Reduction.NotArity -> 
       evd in
-  solve_evar_evar_aux f g env evd pbty ev1 ev2
+  solve_evar_evar_aux force f g env evd pbty ev1 ev2
 
 type conv_fun =
   env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
@@ -1325,7 +1308,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k None ev' ev in
+          let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in
           evdref := evd;
           body
         with
@@ -1342,7 +1325,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
           let evd =
              (* Try to project (a restriction of) the left evar ... *)
             try
-              let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 None ev'' ev' in
+              let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
               let evd = Evd.define evk' body evd in
 		check_evar_instance evd evk' body conv_algo
             with
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee72d31471..9313e22320 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -230,20 +230,20 @@ let evar_instance_array test_id info args =
     else instance_mismatch ()
   | false :: filter, _ :: ctxt ->
     instrec filter ctxt i
-  | true :: filter, (id, _, _) :: ctxt ->
+  | true :: filter, (id,_,_ as d) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      if test_id id c then instrec filter ctxt (succ i)
+      if test_id d c then instrec filter ctxt (succ i)
       else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
   | _ -> instance_mismatch ()
   in
   match Filter.repr (evar_filter info) with
   | None ->
-    let map i (id, _, _) =
+    let map i (id,_,_ as d) =
       if (i < len) then
         let c = Array.unsafe_get args i in
-        if test_id id c then None else Some (id,c)
+        if test_id d c then None else Some (id,c)
       else instance_mismatch ()
     in
     List.map_filter_i map (evar_context info)
@@ -251,7 +251,7 @@ let evar_instance_array test_id info args =
     instrec filter (evar_context info) 0
 
 let make_evar_instance_array info args =
-  evar_instance_array isVarId info args
+  evar_instance_array (fun (id,_,_) -> isVarId id) info args
 
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b6c5d426f9..cf6ba07c60 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -223,7 +223,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6059e9ff84..ec34383820 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -60,13 +60,17 @@ module ReductionBehaviour = struct
 
   let discharge = function
     | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
-       let c' = pop_con c in
-       let vars, _subst, _ctx = Lib.section_segment_of_constant c in
-       let extra = List.length vars in
-       let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
-       let recargs' = List.map ((+) extra) b.b_recargs in
-       let b' = { b with b_nargs = nargs'; b_recargs = recargs' } in
-       Some (ReqGlobal (ConstRef c', req), (ConstRef c', b'))
+      let b =
+        if Lib.is_in_section (ConstRef c) then
+          let vars, _, _ = Lib.section_segment_of_constant c in
+          let extra = List.length vars in
+          let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
+          let recargs' = List.map ((+) extra) b.b_recargs in
+          { b with b_nargs = nargs'; b_recargs = recargs' }
+        else b
+      in
+      let c = Lib.discharge_con c in
+      Some (ReqGlobal (ConstRef c, req), (ConstRef c, b))
     | _ -> None
 
   let rebuild = function
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 223377c277..0e6c595e1a 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -109,7 +109,7 @@ let print_impargs_list prefix l =
 	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
 	   str " applied to " ++
 	   (if Int.equal n1 n2 then int_or_no n2 else
-	    if Int.equal n1 0 then str "less than " ++ int n2
+	    if Int.equal n1 0 then str "no more than " ++ int n2
 	    else int n1 ++ str " to " ++ int_or_no n2) ++
 	    str (String.plural n2 " argument") ++ str ":";
           v 0 (prlist_with_sep cut (fun x -> x)
diff --git a/stm/stm.ml b/stm/stm.ml
index 43db6f3f6c..a4db934b25 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1270,7 +1270,7 @@ end = struct (* {{{ *)
     if TaskQueue.n_workers (Option.get !queue) = 0 then
       if !Flags.compilation_mode = Flags.BuildVio then begin
         let f,assign =
-          Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
+         Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
         let task = ProofTask.(BuildProof {
           t_exn_info; t_start = start; t_stop = stop;
@@ -1281,7 +1281,7 @@ end = struct (* {{{ *)
       end else
         ProofTask.build_proof_here t_exn_info loc stop, cancel_switch
     else 
-      let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in
+      let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
       feedback (Feedback.InProgress 1);
       let task = ProofTask.(BuildProof {
@@ -1436,7 +1436,10 @@ end = struct (* {{{ *)
       let goals, _, _, _, _ = Proof.proof p in
       let open TacTask in
       let res = CList.map_i (fun i g ->
-        let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
+        let f, assign =
+          Future.create_delegate
+            ~name:(Printf.sprintf "subgoal %d" i)
+            (State.exn_on id ~valid:safe_id) in
         let t_ast =
           { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
         let t_name = Goal.uid g in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 04df3b8cda..013270b0bd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2318,7 +2318,10 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let heq = match ido with
       | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env
       | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
-      | IntroIdentifier id -> id in
+      | IntroIdentifier id ->
+          if List.mem id (ids_of_named_context (named_context env)) then
+            user_err_loc (loc,"",pr_id id ++ str" is already used.");
+          id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
       let sigma, eq = Evd.fresh_global env sigma eqdata.eq in
@@ -3769,7 +3772,7 @@ let clear_unselected_context id inhyps cls gl =
       thin ids gl
   | None -> tclIDTAC gl
 
-let use_bindings env sigma elim (c,lbind) typ =
+let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let typ =
     if elim == None then
       (* w/o an scheme, the term has to be applied at least until
@@ -3788,6 +3791,8 @@ let use_bindings env sigma elim (c,lbind) typ =
   let rec find_clause typ =
     try
       let indclause = make_clenv_binding env sigma (c,typ) lbind in
+      if must_be_closed && occur_meta (clenv_value indclause) then
+        error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
       pose_all_metas_as_evars env indclause.evd (clenv_value indclause)
     with e when catchable_exception e ->
@@ -3833,7 +3838,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
   let ccl = Proofview.Goal.raw_concl gl in
   let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
-  let (sigma',c) = use_bindings env sigma elim (c0,lbind) t0 in
+  let (sigma',c) = use_bindings env sigma elim false (c0,lbind) t0 in
   let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
   let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in
   match res with
@@ -3853,7 +3858,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       (Tacticals.New.tclTHENLIST [
         Proofview.Unsafe.tclEVARS sigma;
         Proofview.Refine.refine ~unsafe:true (fun sigma ->
-          let (sigma,c) = use_bindings env sigma elim (c0,lbind) t0 in
+          let b = not with_evars && with_eq != None in
+          let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
           mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t));
         Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
diff --git a/test-suite/bugs/opened/3071.v b/test-suite/bugs/closed/3071.v
index 611ac60655..611ac60655 100644
--- a/test-suite/bugs/opened/3071.v
+++ b/test-suite/bugs/closed/3071.v
diff --git a/test-suite/bugs/closed/3993.v b/test-suite/bugs/closed/3993.v
new file mode 100644
index 0000000000..086d8dd0f3
--- /dev/null
+++ b/test-suite/bugs/closed/3993.v
@@ -0,0 +1,3 @@
+(* Test smooth failure on not fully applied term to destruct with eqn: given *)
+Goal True.
+Fail induction S eqn:H.
diff --git a/test-suite/bugs/closed/4078.v b/test-suite/bugs/closed/4078.v
new file mode 100644
index 0000000000..236cd2fbb1
--- /dev/null
+++ b/test-suite/bugs/closed/4078.v
@@ -0,0 +1,14 @@
+Module Type S.
+
+Axiom foo : nat.
+
+End S.
+
+Module M : S.
+
+Definition bar := 0.
+Definition foo := bar.
+
+End M.
+
+Print All Dependencies M.foo.
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 17f971fda5..d3e48f756e 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -10,14 +10,17 @@ open Util
 open Pp
 open Errors
 
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 51 :
-    (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t)
+    (Vernacexpr.extend_name, deprecation * vernac_command) Hashtbl.t)
 
-let vinterp_add s f =
+let vinterp_add depr s f =
   try
-    Hashtbl.add vernac_tab s f
+    Hashtbl.add vernac_tab s (depr, f)
   with Failure _ ->
     errorlabstrm "vinterp_add"
       (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
@@ -28,7 +31,7 @@ let overwriting_vinterp_add s f =
       let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
     with Not_found -> ()
   end;
-  Hashtbl.add vernac_tab s f
+  Hashtbl.add vernac_tab s (false, f)
 
 let vinterp_map s =
   try
@@ -44,7 +47,16 @@ let vinterp_init () = Hashtbl.clear vernac_tab
 let call ?locality (opn,converted_args) =
   let loc = ref "Looking up command" in
   try
-    let callback = vinterp_map opn in
+    let depr, callback = vinterp_map opn in
+    let () = if depr then
+      let rules = Egramml.get_extend_vernac_rule opn in
+      let pr_gram = function
+      | Egramml.GramTerminal s -> str s
+      | Egramml.GramNonTerminal _ -> str "_"
+      in
+      let pr = pr_sequence pr_gram rules in
+      msg_warning (str "Deprecated vernacular command: " ++ pr)
+    in
     loc:= "Checking arguments";
     let hunk = callback converted_args in
     loc:= "Executing command";
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 38fce5d12b..0282065469 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -8,9 +8,13 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+type deprecation = bool
+type vernac_command = Genarg.raw_generic_argument list -> unit -> unit
+
+val vinterp_add : deprecation -> Vernacexpr.extend_name ->
+  vernac_command -> unit
 val overwriting_vinterp_add :
-  Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit
+  Vernacexpr.extend_name -> vernac_command -> unit
 
 val vinterp_init : unit -> unit
 val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit