Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)

Every time you use abstract a kitten dies, please stop.

1 files changed, 10 insertions, 0 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index e5cfeecdff..c400008113 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -65,6 +65,16 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
+              let add c cb e =
+                let exists c e =
+                  try ignore(Environ.lookup_constant c e); true
+                  with Not_found -> false in 
+                if exists c e then e else Environ.add_constant c cb e in
+              let env = Declareops.fold_side_effects (fun env -> function
+                | SEsubproof (c, cb) -> add c cb env
+                | SEscheme (l,_) ->
+                    List.fold_left (fun e (_,c,cb) -> add c cb e) env l)
+                env (Declareops.uniquize_side_effects eff) in
               let indexes =
 	        search_guard Loc.ghost env
                   possible_indexes fixdecls in