Merge branch 'v8.5'

22 files changed, 186 insertions, 97 deletions

diff --git a/dev/base_include b/dev/base_include
index 197528acdb..767e023ea2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -149,6 +149,7 @@ open Tactic_debug
 open Decl_proof_instr
 open Decl_mode
 
+open Hints
 open Auto
 open Autorewrite
 open Contradiction
diff --git a/engine/evd.ml b/engine/evd.ml
index ce3e91db7f..40409fe7fd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -940,6 +940,9 @@ let add_universe_name evd s l =
 
 let universes evd = UState.ugraph evd.universes
 
+let update_sigma_env evd env =
+  { evd with universes = UState.update_sigma_env evd.universes env }
+
 (* Conversion w.r.t. an evar map and its local universes. *)
 
 let conversion_gen env evd pb t u =
diff --git a/engine/evd.mli b/engine/evd.mli
index b295a431aa..3a95b77f06 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -558,6 +558,8 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub
 
 val nf_constraints : evar_map -> evar_map
 
+val update_sigma_env : evar_map -> env -> evar_map
+
 (** Polymorphic universes *)
 
 val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts
diff --git a/engine/uState.ml b/engine/uState.ml
index 61ab5a8fca..0901d81e9e 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -465,3 +465,11 @@ let universe_of_name uctx s =
 let add_universe_name uctx s l =
   let names' = add_uctx_names s l uctx.uctx_names in
   { uctx with uctx_names = names' }
+
+let update_sigma_env uctx env =
+  let univs = Environ.universes env in
+  let eunivs =
+    { uctx with uctx_initial_universes = univs;
+                         uctx_universes = univs }
+  in
+  merge true univ_rigid eunivs eunivs.uctx_local
diff --git a/engine/uState.mli b/engine/uState.mli
index 6861035fac..3a6f77e14e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -110,6 +110,8 @@ val normalize : t -> t
 
 val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
 
+val update_sigma_env : t -> Environ.env -> t
+
 (** {5 Pretty-printing} *)
 
 val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 8bfc70b63f..d9b84498b7 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -564,7 +564,7 @@ object(self)
         if Queue.is_empty queue then conclude topstack else
         match Queue.pop queue, topstack with
         | `Skip(start,stop), [] ->
-            logger Pp.Error (Richpp.richpp_of_string "You muse close the proof with Qed or Admitted");
+            logger Pp.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
             self#discard_command_queue queue;
             conclude [] 
         | `Skip(start,stop), (_,s) :: topstack ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b71cd31b5c..e0a07dcc3a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -218,8 +218,8 @@ let empty_private_constants = []
 let add_private x xs = x :: xs
 let concat_private xs ys = xs @ ys
 let mk_pure_proof = Term_typing.mk_pure_proof
-let inline_private_constants_in_constr = Term_typing.handle_side_effects
-let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects
+let inline_private_constants_in_constr = Term_typing.inline_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
 let constant_entry_of_private_constant = function
@@ -254,7 +254,9 @@ let universes_of_private eff =
           if cb.const_polymorphic then acc
           else (Univ.ContextSet.of_context cb.const_universes) :: acc)
         acc l
-     | Entries.SEsubproof _ -> acc)
+     | Entries.SEsubproof (c, cb, e) ->
+	if cb.const_polymorphic then acc
+	else Univ.ContextSet.of_context cb.const_universes :: acc)
    [] eff
 
 let env_of_safe_env senv = senv.env
@@ -517,8 +519,7 @@ let add_constant dir l decl senv =
     match decl with
     | ConstantEntry (true, ce) ->
         let exports, ce =
-          Term_typing.validate_side_effects_for_export
-            senv.revstruct senv.env ce in
+          Term_typing.export_side_effects senv.revstruct senv.env ce in
         exports, ConstantEntry (false, ce)
     | _ -> [], decl
   in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d75bd73fb6..a566028d40 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -60,11 +60,11 @@ let rec uniq_seff = function
   | [] -> []
   | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
 (* The list of side effects is in reverse order (most recent first).
- * To keep the "tological" order between effects we have to uniqize from the
- * tail *)
+ * To keep the "topological" order between effects we have to uniq-ize from
+ * the tail *)
 let uniq_seff l = List.rev (uniq_seff (List.rev l))
 
-let handle_side_effects env body ctx side_eff =
+let inline_side_effects env body ctx side_eff =
   let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
     let cbl = match se with
       | SEsubproof (c,cb,b) -> [c,cb,b]
@@ -118,6 +118,8 @@ let handle_side_effects env body ctx side_eff =
   (* CAVEAT: we assure a proper order *)
   List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
 
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct *)
 let check_signatures curmb sl =
   let is_direct_ancestor (sl, curmb) (mb, how_many) =
     match curmb with
@@ -135,7 +137,7 @@ let check_signatures curmb sl =
   let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
   sl
 
-let trust_seff sl b e =
+let skip_trusted_seff sl b e =
   let rec aux sl b e acc =
     match sl, kind_of_term b with
     | (None|Some 0), _ -> b, e, acc
@@ -185,21 +187,21 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body, ctx, signatures =
-            handle_side_effects env body ctx side_eff in
-          let trusted_signatures = check_signatures trust signatures in
-	  let env' = push_context_set ctx env in
+        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+          let body, uctx, signatures =
+            inline_side_effects env body uctx side_eff in
+          let valid_signatures = check_signatures trust signatures in
+	  let env' = push_context_set uctx env in
           let j =
-            let body, env', zip_ctx = trust_seff trusted_signatures body env' in
+            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
             let j = infer env' body in
-            unzip zip_ctx j in
+            unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
 	    (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, ctx) in
+          j.uj_val, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
@@ -210,7 +212,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
       let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
-      let body, ctx, _ = handle_side_effects env body
+      let body, ctx, _ = inline_side_effects env body
         (Univ.ContextSet.union univsctx ctx) side_eff in
       let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
@@ -396,9 +398,9 @@ type side_effect_role =
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+  constant * constant_body * side_effects constant_entry * side_effect_role
 
-let validate_side_effects_for_export mb env ce =
+let export_side_effects mb env ce =
   match ce with
   | ParameterEntry _ | ProjectionEntry _ -> [], ce
   | DefinitionEntry c ->
@@ -481,12 +483,12 @@ let translate_local_def mb env id centry =
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
-let handle_entry_side_effects env ce = { ce with
+let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      let body, ctx',_ = handle_side_effects env body ctx side_eff in
+      let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), []);
 }
 
-let handle_side_effects env body side_eff =
-  pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff)
+let inline_side_effects env body side_eff =
+  pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 509160ccc7..2e6aa161b4 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,30 +19,34 @@ val translate_local_assum : env -> types -> types
 
 val mk_pure_proof : constr -> side_effects proof_output
 
-val handle_side_effects : env -> constr -> side_effects -> constr
+val inline_side_effects : env -> constr -> side_effects -> constr
 (** Returns the term where side effects have been turned into let-ins or beta
     redexes. *)
 
-val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry
-(** Same as {!handle_side_effects} but applied to entries. Only modifies the
+val inline_entry_side_effects :
+  env -> side_effects definition_entry -> side_effects definition_entry
+(** Same as {!inline_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
 val uniq_seff : side_effects -> side_effects
 
-val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body
+val translate_constant :
+  structure_body -> env -> constant -> side_effects constant_entry ->
+    constant_body
 
-(* Checks weather the side effects in constant_entry can be trusted.
- * Returns the list of effects to be exported.
- * Note: It forces the Future.computation.                           *)
 type side_effect_role =
   | Subproof
   | Schema of inductive * string
 
 type exported_side_effect = 
-  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+  constant * constant_body * side_effects constant_entry * side_effect_role
   
-val validate_side_effects_for_export :
+(* Given a constant entry containing side effects it exports them (either
+ * by re-checking them or trusting them).  Returns the constant bodies to
+ * be pushed in the safe_env by safe typing.  The main constant entry
+ * needs to be translated as usual after this step. *)
+val export_side_effects :
   structure_body -> env -> side_effects constant_entry ->
     exported_side_effect list * side_effects constant_entry
 
diff --git a/library/declare.ml b/library/declare.ml
index 63e5a72245..5968fbf38b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -225,9 +225,9 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
-let definition_entry ?(opaque=false) ?(inline=false) ?types
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
-  { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
+  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_polymorphic = poly;
diff --git a/library/declare.mli b/library/declare.mli
index fdbd235614..c6119a58ac 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -48,7 +48,8 @@ type internal_flag =
   | UserIndividualRequest
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
+val definition_entry : ?fix_exn:Future.fix_exn ->
+  ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?poly:polymorphic -> ?univs:Univ.universe_context ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 69593f993c..c94ac846f1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -339,21 +339,6 @@ GEXTEND Gram
       | d = delta_flag -> all_with d
     ] ]
   ;
-  red_tactic:
-    [ [ IDENT "red" -> Red false
-      | IDENT "hnf" -> Hnf
-      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
-      | IDENT "cbv"; s = strategy_flag -> Cbv s
-      | IDENT "cbn"; s = strategy_flag -> Cbn s
-      | IDENT "lazy"; s = strategy_flag -> Lazy s
-      | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
-      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po
-      | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po
-      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
-      | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
-  ;
-  (* This is [red_tactic] including possible extensions *)
   red_expr:
     [ [ IDENT "red" -> Red false
       | IDENT "hnf" -> Hnf
@@ -452,16 +437,6 @@ GEXTEND Gram
     [ [ "using"; l = LIST1 constr SEP "," -> l
       | -> [] ] ]
   ;
-  trivial:
-    [ [ IDENT "trivial" -> Off
-      | IDENT "info_trivial" -> Info
-      | IDENT "debug"; IDENT "trivial" -> Debug ] ]
-  ;
-  auto:
-    [ [ IDENT "auto" -> Off
-      | IDENT "info_auto" -> Info
-      | IDENT "debug"; IDENT "auto" -> Debug ] ]
-  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -627,9 +602,18 @@ GEXTEND Gram
 	  TacAtom (!@loc, TacInductionDestruct(false,true,icl))
 
       (* Automation tactic *)
-      | d = trivial; lems = auto_using; db = hintbases -> TacAtom (!@loc, TacTrivial (d,lems,db))
-      | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-          TacAtom (!@loc, TacAuto (d,n,lems,db))
+      | IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Off, lems, db))
+      | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Info, lems, db))
+      | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacTrivial (Debug, lems, db))
+      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Off, n, lems, db))
+      | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Info, n, lems, db))
+      | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+          TacAtom (!@loc, TacAuto (Debug, n, lems, db))
 
       (* Context management *)
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
@@ -677,7 +661,31 @@ GEXTEND Gram
 	    TacAtom (!@loc, TacInversion (InversionUsing (c,cl), hyp))
 
       (* Conversion *)
-      | r = red_tactic; cl = clause_dft_concl -> TacAtom (!@loc, TacReduce (r, cl))
+      | IDENT "red"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Red false, cl))
+      | IDENT "hnf"; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Hnf, cl))
+      | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Simpl (all_with d, po), cl))
+      | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv s, cl))
+      | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbn s, cl))
+      | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Lazy s, cl))
+      | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Cbv (all_with delta), cl))
+      | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvVm po, cl))
+      | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (CbvNative po, cl))
+      | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Unfold ul, cl))
+      | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Fold l, cl))
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
+          TacAtom (!@loc, TacReduce (Pattern pl, cl))
+
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl ->
 	  let p,cl = merge_occurrences (!@loc) cl oc in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index e036ae3a15..1e0de05dd1 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -703,3 +703,9 @@ 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 a67481e71c..3fbcefd0a4 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -92,6 +92,11 @@ 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_separate:bool -> Future.fix_exn -> closed_proof
diff --git a/stm/stm.ml b/stm/stm.ml
index 7dc0ff84a0..0c0bdc8272 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -123,6 +123,10 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> str""
 
+let update_global_env () =
+  if Proof_global.there_are_pending_proofs () then
+    Proof_global.update_global_env ()
+
 module Vcs_ = Vcs.Make(Stateid)
 type future_proof = Proof_global.closed_proof_output Future.computation
 type proof_mode = string
@@ -135,6 +139,7 @@ type branch_type =
       proof_mode * Stateid.t * Stateid.t  * vernac_qed_type * Vcs_.Branch.t ]
 type cmd_t = {
   ctac : bool; (* is a tactic, needed by the 8.4 semantics of Undo *)
+  ceff : bool; (* is a side-effecting command *)
   cast : ast;
   cids : Id.t list;
   cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
@@ -591,6 +596,7 @@ module State : sig
     ?safe_id:Stateid.t ->
     ?redefine:bool -> ?cache:Summary.marshallable ->
     ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+  val fix_exn_ref : (iexn -> iexn) ref
 
   val install_cached : Stateid.t -> unit
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
@@ -614,6 +620,7 @@ end = struct (* {{{ *)
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
   let cur_id = ref Stateid.dummy
+  let fix_exn_ref = ref (fun x -> x)
 
   (* helpers *)
   let freeze_global_state marshallable =
@@ -721,7 +728,10 @@ end = struct (* {{{ *)
     try
       prerr_endline("defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+      let good_id = match safe_id with None -> !cur_id | Some id -> id in
+      fix_exn_ref := exn_on id ~valid:good_id;
       f ();
+      fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
       prerr_endline ("setting cur id to "^str_id);
@@ -730,7 +740,7 @@ end = struct (* {{{ *)
         Hooks.(call state_computed id ~in_cache:false);
       VCS.reached id true;
       if Proof_global.there_are_pending_proofs () then
-        VCS.goals id (Proof_global.get_open_goals ());
+        VCS.goals id (Proof_global.get_open_goals ())
     with e ->
       let (e, info) = Errors.push e in
       let good_id = !cur_id in
@@ -1753,8 +1763,9 @@ let known_state ?(redefine_qed=false) ~cache id =
   let cherry_pick_non_pstate () =
     Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
     Lib.freeze ~marshallable:`No in
-  let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
-
+  let inject_non_pstate (s,l) =
+    Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
+  in
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
     prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
     reach id;
@@ -1784,9 +1795,9 @@ let known_state ?(redefine_qed=false) ~cache id =
             reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
-      | `Cmd { cast = x } -> (fun () ->
-            reach view.next; vernac_interp id x
-          ), cache, true
+      | `Cmd { cast = x; ceff = eff } -> (fun () ->
+            reach view.next; vernac_interp id x;
+	    if eff then update_global_env ()), cache, true
       | `Fork ((x,_,_,_), None) -> (fun () ->
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
@@ -1885,7 +1896,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
       | `Sideff (`Ast (x,_)) -> (fun () ->
-            reach view.next; vernac_interp id x;
+            reach view.next; vernac_interp id x; update_global_env ()
           ), cache, true
       | `Sideff (`Id origin) -> (fun () ->
             reach view.next;
@@ -2135,7 +2146,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
             else `MainQueue in
-          VCS.commit id (Cmd {ctac=false;cast = x; cids = []; cqueue = queue });
+          VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQuery (false,_), VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
@@ -2158,7 +2169,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           anomaly(str"VtProofMode must be executed VtNow")
       | VtProofMode mode, VtNow ->
           let id = VCS.new_node ~id:newtip () in
-          VCS.commit id (Cmd {ctac=false;cast = x;cids=[];cqueue = `MainQueue});
+          VCS.commit id (Cmd {ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue});
           List.iter
             (fun bn -> match VCS.get_branch bn with
             | { VCS.root; kind = `Master; pos } -> ()
@@ -2176,7 +2187,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtProofStep paral, w ->
           let id = VCS.new_node ~id:newtip () in
           let queue = if paral then `TacQueue (ref false) else `MainQueue in
-          VCS.commit id (Cmd {ctac = true;cast = x;cids = [];cqueue = queue });
+          VCS.commit id (Cmd {ctac = true;ceff = false;cast = x;cids = [];cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtQed keep, w ->
           let valid = if tty then Some(VCS.get_branch_pos head) else None in
@@ -2192,7 +2203,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
       | VtSideff l, w ->
           let id = VCS.new_node ~id:newtip () in
           VCS.checkout VCS.Branch.master;
-          VCS.commit id (Cmd {ctac=false;cast=x;cids=l;cqueue=`MainQueue});
+          VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue});
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2216,7 +2227,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
-              VCS.commit id (Cmd {ctac=false; cast = x; cids = []; cqueue = `MainQueue});
+	      VCS.commit id (Cmd {ctac = false; ceff = true;
+				    cast = x; cids = []; cqueue = `MainQueue});
               VCS.propagate_sideff (Some x);
               VCS.checkout_shallowest_proof_branch ();
             end in
@@ -2551,5 +2563,5 @@ let process_error_hook = Hooks.process_error_hook
 let interp_hook = Hooks.interp_hook
 let with_fail_hook = Hooks.with_fail_hook
 let unreachable_state_hook = Hooks.unreachable_state_hook
-
+let get_fix_exn () = !State.fix_exn_ref
 (* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
index 18ed6fc2e8..0c05c93d4d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -136,3 +136,4 @@ val process_error_hook : Future.fix_exn Hook.t
 val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
   Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
 val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
+val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index dbdfb3e922..0d24b71387 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -214,7 +214,8 @@ type search_state = {
   last_tactic : std_ppcmds Lazy.t;
   dblist : hint_db list;
   localdb :  hint_db list;
-  prev : prev_search_state
+  prev : prev_search_state;
+  local_lemmas : Evd.open_constr list;
 }
 
 and prev_search_state = (* for info eauto *)
@@ -273,7 +274,7 @@ module SearchProblem = struct
 	List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
 				    last_tactic = pp; dblist = s.dblist;
 				    localdb = List.tl s.localdb;
-				    prev = ps}) l
+				    prev = ps; local_lemmas = s.local_lemmas}) l
       in
       let intro_tac =
         let l = filter_tactics s.tacres [Tactics.intro, (-1), lazy (str "intro")] in
@@ -287,7 +288,8 @@ module SearchProblem = struct
 		  hintl (List.hd s.localdb) in
 	     { depth = s.depth; priority = cost; tacres = lgls;
 	       last_tactic = pp; dblist = s.dblist;
-	       localdb = ldb :: List.tl s.localdb; prev = ps })
+	       localdb = ldb :: List.tl s.localdb; prev = ps;
+               local_lemmas = s.local_lemmas})
 	  l
       in
       let rec_tacs =
@@ -299,7 +301,8 @@ module SearchProblem = struct
 	     let nbgl' = List.length (sig_it lgls) in
 	     if nbgl' < nbgl then
 	       { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
-                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb }
+                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
+                  local_lemmas = s.local_lemmas }
 	     else
 	       let newlocal = 
 		 let hyps = pf_hyps g in
@@ -307,12 +310,13 @@ module SearchProblem = struct
 		     let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
 		     let hyps' = pf_hyps gls in
 		       if hyps' == hyps then List.hd s.localdb
-		       else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true [])
+		       else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas)
 		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
 	       in
 		 { depth = pred s.depth; priority = cost; tacres = lgls;
 		   dblist = s.dblist; last_tactic = pp; prev = ps;
-		   localdb = newlocal @ List.tl s.localdb })
+		   localdb = newlocal @ List.tl s.localdb;
+                   local_lemmas = s.local_lemmas })
 	  l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -377,7 +381,7 @@ let pr_info dbg s =
 
 (** Eauto main code *)
 
-let make_initial_state dbg n gl dblist localdb =
+let make_initial_state dbg n gl dblist localdb lems =
   { depth = n;
     priority = 0;
     tacres = tclIDTAC gl;
@@ -385,6 +389,7 @@ let make_initial_state dbg n gl dblist localdb =
     dblist = dblist;
     localdb = [localdb];
     prev = if dbg == Info then Init else Unknown;
+    local_lemmas = lems;
   }
 
 let e_search_auto debug (in_depth,p) lems db_list gl =
@@ -398,7 +403,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
   in
   try
     pr_dbg_header d;
-    let s = tac (make_initial_state d p gl db_list local_db) in
+    let s = tac (make_initial_state d p gl db_list local_db lems) in
     pr_info d s;
     s.tacres
   with Not_found ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b3a17df360..25d80b9c8e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -999,10 +999,12 @@ let interp_induction_arg ist gl arg =
         if Tactics.is_quantified_hypothesis id' gl
         then keep,ElimOnIdent (loc,id')
         else
-          (try keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((constr_of_id env id',NoBindings), sigma, Sigma.refl) }
+          (keep, ElimOnConstr { delayed = begin fun env sigma ->
+          try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
-            user_err_loc (loc,"",
-            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis."))
+            user_err_loc (loc, "interp_induction_arg",
+            pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")
+          end })
       in
       try
         (** FIXME: should be moved to taccoerce *)
diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v
index 5ce1ddf0c4..8175d66ac7 100644
--- a/test-suite/bugs/closed/3267.v
+++ b/test-suite/bugs/closed/3267.v
@@ -34,3 +34,14 @@ Module d.
     debug eauto.
   Defined.
 End d.
+
+(* An other variant which was still failing in 8.5 beta2 *)
+
+Parameter A B : Prop.
+Axiom a:B.
+
+Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end.
+Goal (B -> id A) -> A.
+intros.
+eauto using a.
+Abort.
diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v
new file mode 100644
index 0000000000..3c0b81568a
--- /dev/null
+++ b/test-suite/success/sideff.v
@@ -0,0 +1,12 @@
+Definition idw (A : Type) := A.
+Lemma foobar : unit.
+Proof.
+  Require Import Program.
+  apply (const tt tt).
+Qed.
+
+Lemma foobar' : unit.
+  Lemma aux : forall A : Type, A -> unit.
+  Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed.
+  apply (@aux unit tt).
+Qed.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 73fd3d1a4a..3d338ee0a3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -154,6 +154,7 @@ let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
 let declare_definition ident (local, p, k) ce pl imps hook =
+  let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -170,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k pl imps in
-  Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r
+  Lemmas.call_hook fix_exn hook local r
 
 let _ = Obligations.declare_definition_ref :=
        (fun i k c imps hook -> declare_definition i k c [] imps hook)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0e2de74aa6..de03e8356c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -508,16 +508,17 @@ let declare_definition prg =
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
+  let fix_exn = Stm.get_fix_exn () in
   let ce =
-    definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+    definition_entry ~fix_exn
+     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r ->
-         Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))
-
+      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+      
 open Pp
 
 let rec lam_index n t acc =
@@ -620,8 +621,9 @@ let declare_obligation prg obl body ty uctx =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body else [], body, [||] 
       in
+      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
       let ce = 
-        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants);
+        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
 	  const_entry_polymorphic = poly;