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

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

2 files changed, 0 insertions, 85 deletions

diff --git a/test-suite/bugs/opened/3344.v b/test-suite/bugs/opened/3344.v
deleted file mode 100644
index 8255fd6cce..0000000000
--- a/test-suite/bugs/opened/3344.v
+++ /dev/null
@@ -1,58 +0,0 @@
-(* File reduced by coq-bug-finder from original input, then from 716 lines to 197 lines, then from 206 lines to 162 lines, then from 163 lines to 73 lines *)
-Require Import Coq.Sets.Ensembles.
-Require Import Coq.Strings.String.
-Global Set Implicit Arguments.
-Global Set Asymmetric Patterns.
-Ltac clearbodies := repeat match goal with | [ H := _ |- _ ] => clearbody H end.
-
-Inductive Comp : Type -> Type :=
-| Return : forall A, A -> Comp A
-| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B.
-Inductive computes_to : forall A, Comp A -> A -> Prop :=
-| ReturnComputes : forall A v, @computes_to A (Return v) v
-| BindComputes : forall A B comp_a f comp_a_value comp_b_value,
-                   @computes_to A comp_a comp_a_value
-                   -> @computes_to B (f comp_a_value) comp_b_value
-                   -> @computes_to B (Bind comp_a f) comp_b_value.
-
-Inductive is_computational : forall A, Comp A -> Prop :=
-| Return_is_computational : forall A (x : A), is_computational (Return x)
-| Bind_is_computational : forall A B (cA : Comp A) (f : A -> Comp B),
-                            is_computational cA
-                            -> (forall a,
-                                  @computes_to _ cA a -> is_computational (f a))
-                            -> is_computational (Bind cA f).
-Theorem is_computational_inv A (c : Comp A)
-: is_computational c
-  -> match c with
-       | Return _ _ => True
-       | Bind _ _ x f => is_computational x
-                         /\ forall v, computes_to x v
-                                      -> is_computational (f v)
-     end.
-  admit.
-Defined.
-Fixpoint is_computational_unique_val A (c : Comp A) {struct c}
-: is_computational c -> { a | unique (computes_to c) a }.
-Proof.
-  refine match c as c return is_computational c -> { a | unique (computes_to c) a } with
-           | Return T x => fun _ => exist (unique (computes_to (Return x)))
-                                          x
-                                          _
-           | Bind _ _ x f
-             => fun H
-                => let H' := is_computational_inv H in
-                   let xv := @is_computational_unique_val _ _ (proj1 H') in
-                   let fxv := @is_computational_unique_val _ _ (proj2 H' _ (proj1 (proj2_sig xv))) in
-                   exist (unique (computes_to _))
-                         (proj1_sig fxv)
-                         _
-         end;
-  clearbodies;
-  clear is_computational_unique_val;
-  clear;
-  first [ abstract admit
-        | abstract admit ].
-(* [Fail] does not catch the anomaly *)
-Defined.
-(* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/HoTT_coq_111.v b/test-suite/bugs/opened/HoTT_coq_111.v
deleted file mode 100644
index deb8e61235..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_111.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Module X.
-  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.
-
-  Axioms A B : Type.
-  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.
-End X.
-
-Module Y.
-  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.
-
-  Axioms A B : Type.
-  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.
-End Y.