Tests for #3848 and #3854.

2 files changed, 42 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3848.v b/test-suite/bugs/closed/3848.v
new file mode 100644
index 0000000000..b66aeccaff
--- /dev/null
+++ b/test-suite/bugs/closed/3848.v
@@ -0,0 +1,21 @@
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables A B f g e n.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
+           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b).
+  admit.
+Defined.
+
+Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
+      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
+: (forall b : B, Q b) -> forall a : A, P a.
+Proof.
+  refine (functor_forall
+            (f^-1)
+            (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
+Defined. (* Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/closed/3854.v b/test-suite/bugs/closed/3854.v
new file mode 100644
index 0000000000..f8329cdd20
--- /dev/null
+++ b/test-suite/bugs/closed/3854.v
@@ -0,0 +1,21 @@
+Definition relation (A : Type) := A -> A -> Type.
+Class Reflexive {A} (R : relation A) := reflexivity : forall x : A, R x x.
+Axiom IsHProp : Type -> Type.
+Existing Class IsHProp.
+Inductive Empty : Set := .
+Notation "~ x" := (x -> Empty) : type_scope.
+Record hProp := BuildhProp { type :> Type ; trunc : IsHProp type }.
+Arguments BuildhProp _ {_}.
+Canonical Structure default_hProp := fun T P => (@BuildhProp T P).
+Generalizable Variables A B f g e n.
+Axiom trunc_forall : forall `{P : A -> Type}, IsHProp (forall a, P a).
+Existing Instance trunc_forall.
+Inductive V : Type := | set {A : Type} (f : A -> V) : V.
+Axiom mem : V -> V -> hProp.
+Axiom mem_induction
+: forall (C : V -> hProp), (forall v, (forall x, mem x v -> C x) -> C v) -> forall v, C v.
+Definition irreflexive_mem : forall x, (fun x y => ~ mem x y) x x.
+Proof.
+  pose (fun x => BuildhProp (~ mem x x)).
+  refine (mem_induction (fun x => BuildhProp (~ mem x x)) _); simpl in *.
+  admit.