Merge remote-tracking branch 'v8.6' into trunk

3 files changed, 10 insertions, 8 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a172d2560..0f85dc629 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -404,9 +404,10 @@ let ltac_interp_name_env k0 lvar env =
   (* tail is the part of the env enriched by pretyping *)
   let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
-  let env = pop_rel_context n env in
-  let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
-  push_rel_context ctxt env
+  let open Context.Rel.Declaration in
+  let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in
+  if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
+  else push_rel_context ctxt' (pop_rel_context n env)
 
 let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
@@ -804,8 +805,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         let j = pretype_type empty_valcon env evdref lvar c2 in
           { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
-        let var = (name,j.utj_val) in
-        let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
+        let var = LocalAssum (name, j.utj_val) in
+        let env' = push_rel var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
     let name = ltac_interp_name lvar name in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b6..8259876c2 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
              (h 0 (str "<<" ++ Termops.print_constr x ++
 		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
 		   str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
-		   str ">>") ++ fnl ())
+		   str ">>"))
     in
     let fold () =
       let () = if !debug_RAKAM then
-	  let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
+	  let open Pp in Feedback.msg_notice (str "<><><><><>") in
       (s,cst_l)
     in
     match kind_of_term x with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e9ee55d37..213eecc6b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1081,8 +1081,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
     a
   with e ->
+    let e = CErrors.push e in
     if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
-    raise e
+    iraise e
 
 
 let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env