Merge branch 'v8.5' into trunk

4 files changed, 16 insertions, 7 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 749e0d2b5b..e1c9c2de59 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
     let u = Univ.UContext.instance ctx in
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
-    let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+    let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
       (c, Evd.evar_universe_context sigma), Declareops.no_seff
 
 let build_induction_scheme_in_type dep sort ind =
@@ -63,7 +63,7 @@ let build_induction_scheme_in_type dep sort ind =
   let u = Univ.UContext.instance ctx in
   let ctxset = Univ.ContextSet.of_context ctx in
   let ectx = Evd.evar_universe_context_of ctxset in
-  let sigma, c = build_induction_scheme env (Evd.from_env ~ctx:ectx env) (ind,u) dep sort in
+  let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
     c, Evd.evar_universe_context sigma
  
 let rect_scheme_kind_from_type =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9a64b03fd1..efd6ded44c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -194,7 +194,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     errorlabstrm "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
-  let pf = Proof.start (Evd.from_env ~ctx:(evar_universe_context sigma) invEnv) [invEnv,invGoal] in
+  let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
   let pf =
     fst (Proof.run_tactic env (
       tclTHEN intro (onLastHypId inv_op)) pf)
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 719cc7c98d..aa057a3e86 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1824,8 +1824,8 @@ let declare_projection n instance_id r =
 
 let build_morphism_signature m =
   let env = Global.env () in
-  let m,ctx = Constrintern.interp_constr env Evd.empty m in
-  let sigma = Evd.from_env ~ctx env in
+  let m,ctx = Constrintern.interp_constr env (Evd.from_env env) m in
+  let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
   let cstrs =
     let rec aux t =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4c53d5340b..fea7ab72e4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2222,6 +2222,11 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
   | IntroApplyOn (f,(loc,pat)) ->
       let naming,tac_ipat =
         prepare_intros_loc loc (IntroIdentifier id) destopt pat in
+      let doclear =
+        if naming = NamingMustBe (loc,id) then
+          Proofview.tclUNIT () (* apply_in_once do a replacement *)
+        else
+          Proofview.V82.tactic (clear [id]) in
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
@@ -2230,7 +2235,9 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat) (tac ((dloc,id)::thin) None []))
+                (None,(sigma,(c,NoBindings)))
+                (fun id -> Tacticals.New.tclTHEN doclear (tac_ipat id)))
+             (tac thin None []))
           sigma
       end
 
@@ -2296,7 +2303,9 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
       naming id lemma tac in
   Proofview.Goal.enter begin fun gl ->
-  let destopt = get_previous_hyp_position id gl in
+  let destopt =
+    if with_evars then MoveLast (* evars would depend on the whole context *)
+    else get_previous_hyp_position id gl in
   let naming,ipat_tac = prepare_intros (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in