From 06d4250ec3a62b74c41a4f41deb65e97962f8850 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 11 Jun 2014 13:46:57 +0200
Subject: 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
---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 75fe161507..ba389faa97 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
-- 
cgit v1.2.3