diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 07:59:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 09:57:11 +0100 |
| commit | be5db64b2478a45f0d6bf183b502bc44de709465 (patch) | |
| tree | 55517463cacd4853e24c739376abe06fb315f6fe /tactics | |
| parent | bcff4e5db054caec56acabc9d92ba36a8fc2eff6 (diff) | |
Fixing evars lost in interpretation of eliminator of destruct.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 873f872aa..cc0917010 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1863,7 +1863,9 @@ and interp_atomic ist tac : unit Proofview.tactic = in let sigma,el = Option.fold_map (interp_constr_with_bindings ist env) sigma el in - Tactics.induction_destruct isrec ev (l,el) + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (Tactics.induction_destruct isrec ev (l,el)) end | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in |