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

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

4 files changed, 16 insertions, 9 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 149eeba28..51b7b6f97 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -284,7 +284,7 @@ type side_effects = side_effect list
 let no_seff = ([] : side_effects)
 let iter_side_effects f l = List.iter f (List.rev l)
 let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = CList.uniquize l
+let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
 let union_side_effects l1 l2 = l1 @ l2
 let flatten_side_effects l = List.flatten l
 let side_effects_of_list l = l
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index e5cfeecdf..c40000811 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
diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/closed/3344.v
index 8255fd6cc..8255fd6cc 100644
--- a/test-suite/bugs/opened/3344.v
+++ b/test-suite/bugs/closed/3344.v
diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/closed/HoTT_coq_111.v
index deb8e6123..3b43f31df 100644
--- a/test-suite/bugs/opened/HoTT_coq_111.v
+++ b/test-suite/bugs/closed/HoTT_coq_111.v
@@ -1,5 +1,6 @@
+
 Module X.
-  Set Universe Polymorphism.
+  (*Set Universe Polymorphism.*)
   Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
   Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
 
@@ -7,13 +8,11 @@ Module X.
   Axiom P : A = B.
   Definition foo : A = B.
     abstract (rewrite <- P; reflexivity).
-    (* Error: internal_paths_rew already exists. *)
-  Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-  Admitted.
+  Defined.
 End X.
 
 Module Y.
-  Set Universe Polymorphism.
+  (*Set Universe Polymorphism.*)
   Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
   Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
 
@@ -21,7 +20,5 @@ Module Y.
   Axiom P : A = B.
   Definition foo : (A = B) * (A = B).
     split; abstract (rewrite <- P; reflexivity).
-  (* Error: internal_paths_rew already exists. *)
-  Fail Fail Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
-  Admitted.
+  Defined.
 End Y.