diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 15:27:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-06 16:57:04 +0100 |
| commit | b933f60c2c6b20898becf9cfc7215a610800c75a (patch) | |
| tree | 112255bd3c03b5be620069daf509caa3e6e87b79 | |
| parent | 01be85dd34c59fb0f410e10dc86979fe7a5c583f (diff) | |
Dependency bug in using eqn for destruct.
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 -> |