13 files changed, 386 insertions, 5 deletions

diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/3889.v
new file mode 100644
index 0000000000..6b287324cc
--- /dev/null
+++ b/test-suite/bugs/opened/3889.v
@@ -0,0 +1,11 @@
+Require Import Program.
+
+Inductive Even : nat -> Prop :=
+| evenO : Even O
+| evenS : forall n, Odd n -> Even (S n)
+with Odd : nat -> Prop :=
+| oddS : forall n, Even n -> Odd (S n).
+Axiom admit : forall {T}, T.
+Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit
+with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _.
+Next Obligation of doubleE.
diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v
new file mode 100644
index 0000000000..f9ac9be2c8
--- /dev/null
+++ b/test-suite/bugs/opened/3890.v
@@ -0,0 +1,18 @@
+Class Foo.
+Class Bar := b : Type.
+
+Instance foo : Foo := _.
+(* 1 subgoals, subgoal 1 (ID 4)
+  
+  ============================
+   Foo *)
+
+Instance bar : Bar.
+exact Type.
+Defined.
+(* bar is defined *)
+
+About foo.
+(* foo not a defined object. *)
+
+Fail Defined.
diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v
new file mode 100644
index 0000000000..fd95503e6b
--- /dev/null
+++ b/test-suite/bugs/opened/3916.v
@@ -0,0 +1,3 @@
+Require Import List.
+
+Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *)
diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/3919.v-disabled
new file mode 100644
index 0000000000..0d661de9c4
--- /dev/null
+++ b/test-suite/bugs/opened/3919.v-disabled
@@ -0,0 +1,13 @@
+Require Import MSets.
+Require Import Orders.
+
+Declare Module Signal : OrderedType.
+
+Module S := MSetAVL.Make(Signal).
+Module Sdec := Decide(S).
+Export Sdec.
+
+Hint Extern 0 (Signal.eq ?x ?y) => now symmetry.
+
+Goal forall o s, Signal.eq o s.
+Proof. fsetdec. Qed.
diff --git a/test-suite/bugs/opened/3922.v-disabled b/test-suite/bugs/opened/3922.v-disabled
new file mode 100644
index 0000000000..ce4f509cad
--- /dev/null
+++ b/test-suite/bugs/opened/3922.v-disabled
@@ -0,0 +1,83 @@
+Set Universe Polymorphism.
+Notation Type0 := Set.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Local Open Scope trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc -2).
+Notation IsHProp := (IsTrunc -1).
+
+Monomorphic Axiom dummy_funext_type : Type0.
+Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+  trunctype_type : Type ;
+  istrunc_trunctype_type : IsTrunc n trunctype_type
+}.
+
+Arguments BuildTruncType _ _ {_}.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (-1)-Type.
+
+Notation BuildhProp := (BuildTruncType -1).
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+: IsTrunc@{j} n (Trunc@{i} n A).
+Admitted.
+
+Definition Trunc_ind {n A}
+  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+  : (forall a, P (tr a)) -> (forall aa, P aa)
+:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
+           (P : Type) `{Pc : X -> Contr P}
+           (g : X -> P) (h : P -> Y) (p : h o g == f)
+: Unit.
+Proof.
+  assert (merely X -> IsHProp P) by admit.
+  refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _);
+    [ assumption.. | ].
+  Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P).
diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/opened/3923.v
new file mode 100644
index 0000000000..6aa6b4932e
--- /dev/null
+++ b/test-suite/bugs/opened/3923.v
@@ -0,0 +1,33 @@
+Module Type TRIVIAL.
+Parameter t:Type.
+End TRIVIAL.
+
+Module MkStore (Key : TRIVIAL).
+
+Module St : TRIVIAL.
+Definition t := unit.
+End St.
+
+End MkStore.
+
+
+
+Module Type CERTRUNTIMETYPES (B  : TRIVIAL).
+
+Parameter cert_fieldstore : Type.
+Parameter empty_fieldstore : cert_fieldstore.
+
+End CERTRUNTIMETYPES.
+
+
+
+Module MkCertRuntimeTypes (B  : TRIVIAL) : CERTRUNTIMETYPES B.
+
+Module FieldStore := MkStore B.
+
+Definition cert_fieldstore := FieldStore.St.t.
+Axiom empty_fieldstore : cert_fieldstore.
+
+End MkCertRuntimeTypes.
+
+Fail Extraction MkCertRuntimeTypes.
diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v
new file mode 100644
index 0000000000..cfad763572
--- /dev/null
+++ b/test-suite/bugs/opened/3926.v
@@ -0,0 +1,30 @@
+Notation compose := (fun g f x => g (f x)).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
+Local Open Scope equiv_scope.
+Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x.
+Generalizable Variables A B C f g.
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000
+  := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1).
+Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g
+  := Build_IsEquiv _ _ g (f ^-1).
+Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000
+  := Build_IsEquiv B A f^-1 f.
+Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}
+  `{IsEquiv A B f} `{IsEquiv A C (g o f)}
+  : IsEquiv g.
+Proof.
+  Unset Typeclasses Modulo Eta.
+  exact (isequiv_homotopic (compose (compose g f) f^-1)
+                           (fun b => ap g (eisretr f b))) || fail "too early".
+  Undo.
+  Set Typeclasses Modulo Eta.
+  Set Typeclasses Dependency Order.
+  Set Typeclasses Debug.
+  Fail exact (isequiv_homotopic (compose (compose g f) f^-1)
+                           (fun b => ap g (eisretr f b))).
diff --git a/test-suite/bugs/opened/3928.v-disabled b/test-suite/bugs/opened/3928.v-disabled
new file mode 100644
index 0000000000..b470eb229b
--- /dev/null
+++ b/test-suite/bugs/opened/3928.v-disabled
@@ -0,0 +1,12 @@
+Typeclasses eauto := bfs.
+
+Class Foo := {}.
+Class Bar := {}.
+
+Instance: Bar.
+Instance: Foo -> Bar -> Foo -> Foo | 1.
+Instance: Bar -> Foo | 100.
+Instance: Foo -> Bar -> Foo -> Foo | 1.
+
+Set Typeclasses Debug.
+Timeout 1 Check (_ : Foo). (* timeout *)
diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/3938.v
new file mode 100644
index 0000000000..2d0d1930f1
--- /dev/null
+++ b/test-suite/bugs/opened/3938.v
@@ -0,0 +1,6 @@
+Require Import Coq.Arith.PeanoNat.
+Hint Extern 1 => admit : typeclass_instances.
+Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b.
+  intros a b f H.
+  rewrite H. (* Toplevel input, characters 15-25:
+Anomaly: Evar ?X11 was not declared. Please report. *)
diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v
new file mode 100644
index 0000000000..e77bdbc652
--- /dev/null
+++ b/test-suite/bugs/opened/3946.v
@@ -0,0 +1,11 @@
+Require Import ZArith.
+
+Inductive foo := Foo : Z.le 0 1 -> foo.
+
+Definition bar (f : foo) := let (f) := f in f.
+
+(* Doesn't work: *)
+(* Arguments bar f.*)
+
+(* Does work *)
+Arguments bar f _.
diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v
new file mode 100644
index 0000000000..165813084d
--- /dev/null
+++ b/test-suite/bugs/opened/3948.v
@@ -0,0 +1,25 @@
+Module Type S.
+Parameter t : Type.
+End S.
+
+Module Bar(X : S).
+Proof.
+  Definition elt := X.t.
+  Axiom fold : elt.
+End Bar.
+
+Module Make (X: S) := Bar(X).
+
+Declare Module X : S.
+
+Module Type Interface.
+  Parameter constant : unit.
+End Interface.
+
+Module DepMap : Interface.
+  Module Dom := Make(X).
+  Definition constant : unit :=
+    let _ := @Dom.fold in tt.
+End DepMap.
+
+Print Assumptions DepMap.constant.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3956.v b/test-suite/bugs/opened/3956.v
new file mode 100644
index 0000000000..94c0c6744c
--- /dev/null
+++ b/test-suite/bugs/opened/3956.v
@@ -0,0 +1,141 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+Set Universe Polymorphism.
+Set Primitive Projections.
+Close Scope nat_scope.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {A B} _ _.
+Arguments fst {A B} _ / .
+Arguments snd {A B} _ / .
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+Definition Type2 := Eval hnf in let gt := (Type1 : Type@{i}) in Type@{i}.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+Definition concat {A} {x y z : A} (p : x = y) (q : y = z) : x = z
+  := match p, q with idpath, idpath => idpath end.
+
+Definition path_prod {A B : Type} (z z' : A * B)
+: (fst z = fst z') -> (snd z = snd z') -> (z = z').
+Proof.
+  destruct z, z'; simpl; intros [] []; reflexivity.
+Defined.  
+
+Module Type TypeM.
+  Parameter m : Type2.
+End TypeM.
+
+Module ProdM (XM : TypeM) (YM : TypeM) <: TypeM.
+  Definition m := XM.m * YM.m.
+End ProdM.
+
+Module Type FunctionM (XM YM : TypeM).
+  Parameter m : XM.m -> YM.m.
+End FunctionM.
+
+Module IdmapM (XM : TypeM) <: FunctionM XM XM.
+  Definition m := (fun x => x) : XM.m -> XM.m.
+End IdmapM.
+
+Module Type HomotopyM (XM YM : TypeM) (fM gM : FunctionM XM YM).
+  Parameter m : forall x, fM.m x = gM.m x.
+End HomotopyM.
+
+Module ComposeM (XM YM ZM : TypeM)
+       (gM : FunctionM YM ZM) (fM : FunctionM XM YM)
+       <: FunctionM XM ZM.
+  Definition m := (fun x => gM.m (fM.m x)).
+End ComposeM.
+
+Module Type CorecM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (gM : FunctionM XM ZM).
+  Parameter m : XM.m -> YM.m.
+  Parameter m_beta : forall x, fM.m (m x) = gM.m x.
+End CorecM.
+
+Module Type CoindpathsM (YM ZM : TypeM) (fM : FunctionM YM ZM)
+       (XM : TypeM) (hM kM : FunctionM XM YM).
+  Module fhM := ComposeM XM YM ZM fM hM.
+  Module fkM := ComposeM XM YM ZM fM kM.
+  Declare Module mM (pM : HomotopyM XM ZM fhM fkM)
+    : HomotopyM XM YM hM kM.
+End CoindpathsM.
+
+Module Type Comodality (XM : TypeM).
+  Parameter m : Type2.
+  Module mM <: TypeM.
+    Definition m := m.
+  End mM.
+  Parameter from : m -> XM.m.
+  Module fromM <: FunctionM mM XM.
+    Definition m := from.
+  End fromM.
+  Declare Module corecM : CorecM mM XM fromM.
+  Declare Module coindpathsM : CoindpathsM mM XM fromM.
+End Comodality.
+
+Module Comodality_Theory (F : Comodality).
+
+  Module F_functor_M (XM YM : TypeM) (fM : FunctionM XM YM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module f_o_from_M <: FunctionM FXM.mM YM.
+      Definition m := fun x => fM.m (FXM.from x).
+    End f_o_from_M.
+    Module mM := FYM.corecM FXM.mM f_o_from_M.
+    Definition m := mM.m.
+  End F_functor_M.
+
+  Module F_prod_cmp_M (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    Module PM := ProdM XM YM.
+    Module PFM := ProdM FXM FYM.
+    Module fstM <: FunctionM PM XM.
+      Definition m := @fst XM.m YM.m.
+    End fstM.
+    Module sndM <: FunctionM PM YM.
+      Definition m := @snd XM.m YM.m.
+    End sndM.
+    Module FPM := F PM.
+    Module FfstM := F_functor_M PM XM fstM FPM FXM.
+    Module FsndM := F_functor_M PM YM sndM FPM FYM.
+    Definition m : FPM.m -> PFM.m
+      := fun z => (FfstM.m z , FsndM.m z).
+  End F_prod_cmp_M.
+
+  Module isequiv_F_prod_cmp_M
+         (XM YM : TypeM)
+         (FXM : Comodality XM) (FYM : Comodality YM).
+    (** The comparison map *)
+    Module cmpM := F_prod_cmp_M XM YM FXM FYM.
+    Module FPM := cmpM.FPM.
+    (** We construct an inverse to it using corecursion. *)
+    Module prod_from_M <: FunctionM cmpM.PFM cmpM.PM.
+      Definition m : cmpM.PFM.m -> cmpM.PM.m
+        := fun z => ( FXM.from (fst z) , FYM.from (snd z) ).
+    End prod_from_M.
+    Module cmpinvM <: FunctionM cmpM.PFM FPM
+      := FPM.corecM cmpM.PFM prod_from_M.
+    (** We prove the first homotopy *)
+    Module cmpinv_o_cmp_M <: FunctionM FPM FPM
+      := ComposeM FPM cmpM.PFM FPM cmpinvM cmpM.
+    Module idmap_FPM <: FunctionM FPM FPM
+      := IdmapM FPM.
+    Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
+    Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
+      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+      Proof.
+        intros x.
+        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+        apply path_prod@{i i i}; simpl.
+        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
+        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+      Defined.
+    Fail End cip_FPHM.
+(*  End isequiv_F_prod_cmp_M.
+
+End Comodality_Theory.*)
diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v
deleted file mode 100644
index 3daf452132..0000000000
--- a/test-suite/bugs/opened/4214.v
+++ /dev/null
@@ -1,5 +0,0 @@
-(* Check that subst uses all equations around *)
-Goal forall A (a b c : A), b = a -> b = c -> a = c.
-intros.
-subst.
-Fail reflexivity.