From b933f60c2c6b20898becf9cfc7215a610800c75a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 6 Nov 2014 15:27:51 +0100
Subject: Dependency bug in using eqn for destruct.

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f2459fc8..d14730e4c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2308,7 +2308,7 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
       let sigma, refl = Evd.fresh_global env sigma eqdata.refl in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
-      let newenv = insert_before [id,body,t;heq,None,eq] lastlhyp env in
+      let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in
       let (sigma,x) = new_evar newenv sigma ~principal:true ccl in
       (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
   | None ->
-- 
cgit v1.2.3