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

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4aa7ffa7b..2c97cf442 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
-- 
cgit v1.2.3