From eb479438328a473ff1cf5fe010ed714194dbf28f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 00:50:19 +0200
Subject: [pp] Fix newline issues.

This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where
we got a few cases wrong wrt to newline endings.

Thanks to @herbelin for pointing it out.

This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
---
 pretyping/reductionops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b61..8259876c29 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
-- 
cgit v1.2.3


From 00808a1fa05e34fee36b8dfff4e7c72943b22c23 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 18:54:39 +0200
Subject: Short path for Pretyping.ltac_interp_name_env.

Instead of recomputing the evar name environment from scratch when it is
unchanged, we simply return the original one.

This should fix #4964 for good, although I still find the global evar naming
mechanism from Pretyping more than messy. Introducing the heuristic allowing
to capture variables from Ltac in constr binders is indeed the root of many
evils... That is far from being a zero-cost abstraction!
---
 pretyping/pretyping.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ef96e0344..e7f87c5f71 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -403,9 +403,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
-- 
cgit v1.2.3


From b1791fe718eae95897d2dbd160b05285c6df239c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 21 Aug 2016 19:33:03 +0200
Subject: Do not recompute the whole evar naming environment in GProd
 intepretation.

---
 pretyping/pretyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e7f87c5f71..f466740036 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -804,8 +804,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
-- 
cgit v1.2.3


From 687d510cb43db5029fb4545c3b12ac20cf99197a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 22 Aug 2016 11:11:41 +0200
Subject: Pushing error backtrace in unification reraise.

---
 pretyping/unification.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f8..6d80db6455 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1080,8 +1080,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
-- 
cgit v1.2.3