diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-11 13:46:57 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-11 13:46:57 +0200 |
| commit | 06d4250ec3a62b74c41a4f41deb65e97962f8850 (patch) | |
| tree | bf42ab68083a53303d82e9a94afe3710cc6dc4a5 | |
| parent | 1d9a159b64497c838618753ca1696e1f5f8937fe (diff) | |
fix handling of side effects in abstract (fixes QArithSternBrocot)
The right fix should probably be to remove the build_constant_by_tactic
function and only use the build_by_tactic one
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 75fe16150..ba389faa9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3828,7 +3828,8 @@ let abstract_subproof id gk tac = let evd = Evd.merge_universe_subst evd subst in let open Declareops in let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff no_seff in + let effs = cons_side_effects eff + Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = Proofview.V82.tclEVARS evd <*> Proofview.tclEFFECTS effs <*> new_exact_no_check (applist (lem, args)) in |