From bc7ffd368789cb82bb8fc8b642b3de870b92c897 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 17 Aug 2016 10:30:00 +0200
Subject: Fixing #3070 ("subst" taking properly into account chains of
 dependencies).

---
 tactics/equality.ml           | 2 +-
 test-suite/bugs/closed/3070.v | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3070.v

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4aa7ffa7bd..2c97cf4425 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1691,7 +1691,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
          && List.exists (fun y -> occur_var_in_decl env y dcl) deps
       then
         let id_dest = if !regular_subst_tactic then dest else MoveLast in
-        (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps)
+        (dest,id::deps,(id_dest,id)::allhyps)
       else
         (MoveBefore id,deps,allhyps))
       hyps
diff --git a/test-suite/bugs/closed/3070.v b/test-suite/bugs/closed/3070.v
new file mode 100644
index 0000000000..7a8feca587
--- /dev/null
+++ b/test-suite/bugs/closed/3070.v
@@ -0,0 +1,6 @@
+(* Testing subst wrt chains of dependencies *)
+
+Lemma foo (a1 a2 : Set) (b1 : a1 -> Prop)
+      (Ha : a1 = a2) (c : a1) (d : b1 c) : True.
+Proof.
+  subst.
-- 
cgit v1.2.3