9 files changed, 537 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_4157.v b/test-suite/bugs/closed/bug_4157.v
new file mode 100644
index 0000000000..a9e96fcdde
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4157.v
@@ -0,0 +1,272 @@
+(** The following proof is due to a bug in `vm_compute` and was found by
+    Maxime Dénès and Pierre-Marie Pédrot. *)
+Inductive t :=
+| C_0 : nat -> t
+| C_1 : nat -> t
+| C_2 : nat -> t
+| C_3 : nat -> t
+| C_4 : nat -> t
+| C_5 : nat -> t
+| C_6 : nat -> t
+| C_7 : nat -> t
+| C_8 : nat -> t
+| C_9 : nat -> t
+| C_10 : nat -> t
+| C_11 : nat -> t
+| C_12 : nat -> t
+| C_13 : nat -> t
+| C_14 : nat -> t
+| C_15 : nat -> t
+| C_16 : nat -> t
+| C_17 : nat -> t
+| C_18 : nat -> t
+| C_19 : nat -> t
+| C_20 : nat -> t
+| C_21 : nat -> t
+| C_22 : nat -> t
+| C_23 : nat -> t
+| C_24 : nat -> t
+| C_25 : nat -> t
+| C_26 : nat -> t
+| C_27 : nat -> t
+| C_28 : nat -> t
+| C_29 : nat -> t
+| C_30 : nat -> t
+| C_31 : nat -> t
+| C_32 : nat -> t
+| C_33 : nat -> t
+| C_34 : nat -> t
+| C_35 : nat -> t
+| C_36 : nat -> t
+| C_37 : nat -> t
+| C_38 : nat -> t
+| C_39 : nat -> t
+| C_40 : nat -> t
+| C_41 : nat -> t
+| C_42 : nat -> t
+| C_43 : nat -> t
+| C_44 : nat -> t
+| C_45 : nat -> t
+| C_46 : nat -> t
+| C_47 : nat -> t
+| C_48 : nat -> t
+| C_49 : nat -> t
+| C_50 : nat -> t
+| C_51 : nat -> t
+| C_52 : nat -> t
+| C_53 : nat -> t
+| C_54 : nat -> t
+| C_55 : nat -> t
+| C_56 : nat -> t
+| C_57 : nat -> t
+| C_58 : nat -> t
+| C_59 : nat -> t
+| C_60 : nat -> t
+| C_61 : nat -> t
+| C_62 : nat -> t
+| C_63 : nat -> t
+| C_64 : nat -> t
+| C_65 : nat -> t
+| C_66 : nat -> t
+| C_67 : nat -> t
+| C_68 : nat -> t
+| C_69 : nat -> t
+| C_70 : nat -> t
+| C_71 : nat -> t
+| C_72 : nat -> t
+| C_73 : nat -> t
+| C_74 : nat -> t
+| C_75 : nat -> t
+| C_76 : nat -> t
+| C_77 : nat -> t
+| C_78 : nat -> t
+| C_79 : nat -> t
+| C_80 : nat -> t
+| C_81 : nat -> t
+| C_82 : nat -> t
+| C_83 : nat -> t
+| C_84 : nat -> t
+| C_85 : nat -> t
+| C_86 : nat -> t
+| C_87 : nat -> t
+| C_88 : nat -> t
+| C_89 : nat -> t
+| C_90 : nat -> t
+| C_91 : nat -> t
+| C_92 : nat -> t
+| C_93 : nat -> t
+| C_94 : nat -> t
+| C_95 : nat -> t
+| C_96 : nat -> t
+| C_97 : nat -> t
+| C_98 : nat -> t
+| C_99 : nat -> t
+| C_100 : nat -> t
+| C_101 : nat -> t
+| C_102 : nat -> t
+| C_103 : nat -> t
+| C_104 : nat -> t
+| C_105 : nat -> t
+| C_106 : nat -> t
+| C_107 : nat -> t
+| C_108 : nat -> t
+| C_109 : nat -> t
+| C_110 : nat -> t
+| C_111 : nat -> t
+| C_112 : nat -> t
+| C_113 : nat -> t
+| C_114 : nat -> t
+| C_115 : nat -> t
+| C_116 : nat -> t
+| C_117 : nat -> t
+| C_118 : nat -> t
+| C_119 : nat -> t
+| C_120 : nat -> t
+| C_121 : nat -> t
+| C_122 : nat -> t
+| C_123 : nat -> t
+| C_124 : nat -> t
+| C_125 : nat -> t
+| C_126 : nat -> t
+| C_127 : nat -> t
+| C_128 : nat -> t
+| C_129 : nat -> t
+| C_130 : nat -> t
+| C_131 : nat -> t
+| C_132 : nat -> t
+| C_133 : nat -> t
+| C_134 : nat -> t
+| C_135 : nat -> t
+| C_136 : nat -> t
+| C_137 : nat -> t
+| C_138 : nat -> t
+| C_139 : nat -> t
+| C_140 : nat -> t
+| C_141 : nat -> t
+| C_142 : nat -> t
+| C_143 : nat -> t
+| C_144 : nat -> t
+| C_145 : nat -> t
+| C_146 : nat -> t
+| C_147 : nat -> t
+| C_148 : nat -> t
+| C_149 : nat -> t
+| C_150 : nat -> t
+| C_151 : nat -> t
+| C_152 : nat -> t
+| C_153 : nat -> t
+| C_154 : nat -> t
+| C_155 : nat -> t
+| C_156 : nat -> t
+| C_157 : nat -> t
+| C_158 : nat -> t
+| C_159 : nat -> t
+| C_160 : nat -> t
+| C_161 : nat -> t
+| C_162 : nat -> t
+| C_163 : nat -> t
+| C_164 : nat -> t
+| C_165 : nat -> t
+| C_166 : nat -> t
+| C_167 : nat -> t
+| C_168 : nat -> t
+| C_169 : nat -> t
+| C_170 : nat -> t
+| C_171 : nat -> t
+| C_172 : nat -> t
+| C_173 : nat -> t
+| C_174 : nat -> t
+| C_175 : nat -> t
+| C_176 : nat -> t
+| C_177 : nat -> t
+| C_178 : nat -> t
+| C_179 : nat -> t
+| C_180 : nat -> t
+| C_181 : nat -> t
+| C_182 : nat -> t
+| C_183 : nat -> t
+| C_184 : nat -> t
+| C_185 : nat -> t
+| C_186 : nat -> t
+| C_187 : nat -> t
+| C_188 : nat -> t
+| C_189 : nat -> t
+| C_190 : nat -> t
+| C_191 : nat -> t
+| C_192 : nat -> t
+| C_193 : nat -> t
+| C_194 : nat -> t
+| C_195 : nat -> t
+| C_196 : nat -> t
+| C_197 : nat -> t
+| C_198 : nat -> t
+| C_199 : nat -> t
+| C_200 : nat -> t
+| C_201 : nat -> t
+| C_202 : nat -> t
+| C_203 : nat -> t
+| C_204 : nat -> t
+| C_205 : nat -> t
+| C_206 : nat -> t
+| C_207 : nat -> t
+| C_208 : nat -> t
+| C_209 : nat -> t
+| C_210 : nat -> t
+| C_211 : nat -> t
+| C_212 : nat -> t
+| C_213 : nat -> t
+| C_214 : nat -> t
+| C_215 : nat -> t
+| C_216 : nat -> t
+| C_217 : nat -> t
+| C_218 : nat -> t
+| C_219 : nat -> t
+| C_220 : nat -> t
+| C_221 : nat -> t
+| C_222 : nat -> t
+| C_223 : nat -> t
+| C_224 : nat -> t
+| C_225 : nat -> t
+| C_226 : nat -> t
+| C_227 : nat -> t
+| C_228 : nat -> t
+| C_229 : nat -> t
+| C_230 : nat -> t
+| C_231 : nat -> t
+| C_232 : nat -> t
+| C_233 : nat -> t
+| C_234 : nat -> t
+| C_235 : nat -> t
+| C_236 : nat -> t
+| C_237 : nat -> t
+| C_238 : nat -> t
+| C_239 : nat -> t
+| C_240 : nat -> t
+| C_241 : nat -> t
+| C_242 : nat -> t
+| C_243 : nat -> t
+| C_244 : nat -> t
+| C_245 : nat -> t
+| C_246 : nat -> t
+| C_247 : nat -> t
+| C_248 : nat -> t
+| C_249 : nat -> t
+| C_250 : nat -> t
+| C_251 : nat -> t
+| C_252 : nat -> t
+| C_253 : nat -> t
+| C_254 : nat -> t
+| C_255 : nat -> t
+| C_256 : nat -> t.
+
+Definition is_256 (x : t) : bool :=
+  match x with
+  | C_256 _ => true
+  | _ => false
+  end.
+
+Lemma falso : False.
+  assert (is_256 (C_256 0) = true) by reflexivity.
+  (* The next line was successful in 8.2pl3 *)
+  Fail assert (is_256 (C_256 0) = false) by (vm_compute; reflexivity).
+Abort.
diff --git a/test-suite/bugs/closed/bug_9598.v b/test-suite/bugs/closed/bug_9598.v
new file mode 100644
index 0000000000..00bbfcf5d9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9598.v
@@ -0,0 +1,36 @@
+Module case.
+
+  Inductive pair := K (n1 : nat) (n2 : nat).
+  Definition fst (p : pair) : nat := match p with K n _ => n end.
+
+  Definition alias_K a b := K a b.
+
+  Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)).
+  Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)).
+
+End case.
+
+Module fixpoint.
+
+  Inductive pair := K (n1 : nat) (n2 : nat).
+  Fixpoint fst (p : pair) : nat := match p with K n _ => n end.
+
+  Definition alias_K a b := K a b.
+
+  Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)).
+  Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)).
+
+End fixpoint.
+
+Module primproj.
+
+  Set Primitive Projections.
+
+  Inductive pair := K { fst : nat; snd : nat }.
+
+  Definition alias_K a b := K a b.
+
+  Fixpoint rec (x : nat) : nat := fst (K 0 (rec x)).
+  Fixpoint rec_ko (x : nat) : nat := fst (alias_K 0 (rec_ko x)).
+
+End primproj.
diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v
new file mode 100644
index 0000000000..b5fa601278
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9663.v
@@ -0,0 +1,2 @@
+Definition id_depfn S T (f : forall x : S, T x) := f.
+Definition idn : nat -> nat := @id_depfn _ _ (fun x => x).
diff --git a/test-suite/output/Error_msg_diffs.out b/test-suite/output/Error_msg_diffs.out
new file mode 100644
index 0000000000..3e337e892d
--- /dev/null
+++ b/test-suite/output/Error_msg_diffs.out
@@ -0,0 +1,12 @@
+File "stdin", line 32, characters 0-12:
+Error:
+In environment
+T : Type
+p : T -> bool
+a : T
+t1, t2 : btree T
+IH1 : count p (rev_tree t1) = count p t1
+IH2 : count p (rev_tree t2) = count p t2
+Unable to unify "(if p a then 1 else 0) + (count p t1 + count p t2)" with
+ "(if p a then 1 else 0) + (count p t2 + count p t1)".
+
diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
new file mode 100644
index 0000000000..11c766b210
--- /dev/null
+++ b/test-suite/output/Error_msg_diffs.v
@@ -0,0 +1,35 @@
+(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
+(* Shows diffs in an error message for an "Unable to unify" error *)
+Require Import Arith List Bool.
+
+Inductive btree (T : Type) : Type :=
+  Leaf | Node (val : T) (t1 t2 : btree T).
+
+Arguments Leaf {T}.
+Arguments Node {T}.
+
+Fixpoint rev_tree {T : Type} (t : btree T) : btree T :=
+match t with
+| Leaf => Leaf
+| Node x t1 t2 => Node x (rev_tree t2) (rev_tree t1)
+end.
+
+Fixpoint count {T : Type} (p : T -> bool) (t : btree T) : nat :=
+match t with
+| Leaf => 0
+| Node x t1 t2 =>
+  (if p x then 1 else 0) + (count p t1 + count p t2)
+end.
+
+Lemma count_rev_tree {T} (p : T -> bool) t : count p (rev_tree t) = count p t.
+Proof.
+induction t as [ | a t1 IH1 t2 IH2].
+  easy.
+simpl.
+rewrite IH1.
+rewrite IH2.
+reflexivity.
+rewrite (Nat.add_comm (count p t2)).
+easy.
+Qed.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
new file mode 100644
index 0000000000..2a7ce806d7
--- /dev/null
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -0,0 +1,33 @@
+File "stdin", line 10, characters 0-28:
+Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker]
+[ab] : A >-> B
+[ab; bd] : A >-> D
+[ac] : A >-> C
+[bd] : B >-> D
+[cd] : C >-> D
+[B_A] : B >-> A
+[C_A] : C >-> A
+[D_B] : D >-> B
+[D_A] : D >-> A
+[D_C] : D >-> C
+[A'_A] : A' >-> A
+[B_A'] : B >-> A'
+[B_A'; A'_A] : B >-> A
+[C_A'] : C >-> A'
+[C_A'; A'_A] : C >-> A
+[D_B; B_A'] : D >-> A'
+[D_A] : D >-> A
+[D_B] : D >-> B
+[D_C] : D >-> C
+File "stdin", line 103, characters 0-86:
+Warning: Ambiguous paths: [D_C; C_A'] : D >-> A'
+[ambiguous-paths,typechecker]
+[A'_A] : A' >-> A
+[B_A'] : B >-> A'
+[B_A'; A'_A] : B >-> A
+[C_A'] : C >-> A'
+[C_A'; A'_A] : C >-> A
+[D_B; B_A'] : D >-> A'
+[D_A] : D >-> A
+[D_B] : D >-> B
+[D_C] : D >-> C
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
new file mode 100644
index 0000000000..a4af27539c
--- /dev/null
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -0,0 +1,109 @@
+Module test1.
+Section test1.
+
+Variable (A B C D : Type).
+Variable (ab : A -> B) (bd : B -> D) (ac : A -> C) (cd : C -> D).
+
+Local Coercion ab : A >-> B.
+Local Coercion bd : B >-> D.
+Local Coercion ac : A >-> C.
+Local Coercion cd : C >-> D.
+
+Print Graph.
+
+End test1.
+End test1.
+
+Module test2.
+Section test2.
+Variable (A : Type) (P Q : A -> Prop).
+
+Record B := {
+  B_A : A;
+  B_P : P B_A }.
+
+Record C := {
+  C_A : A;
+  C_Q : Q C_A }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion B_A : B >-> A.
+Local Coercion C_A : C >-> A.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B := Build_B (D_A d) (D_P d).
+Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
+
+Variable (A : Type) (P Q : A -> Prop).
+
+Definition A' (x : bool) := A.
+
+Record B (x : bool) := {
+  B_A' : A' x;
+  B_P : P B_A' }.
+
+Record C (x : bool) := {
+  C_A' : A' x;
+  C_Q : Q C_A' }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion A'_A (x : bool) (a : A' x) : A := a.
+Local Coercion B_A' : B >-> A'.
+Local Coercion C_A' : C >-> A'.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B false := Build_B false (D_A d) (D_P d).
+Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
+
+Print Graph.
+
+End test3.
+End test3.
+
+Module test4.
+Section test4.
+
+Variable (A : Type) (P Q : A -> Prop).
+
+Record A' (x : bool) := { A'_A : A }.
+
+Record B (x : bool) := {
+  B_A' : A' x;
+  B_P : P (A'_A x B_A') }.
+
+Record C (x : bool) := {
+  C_A' : A' x;
+  C_Q : Q (A'_A x C_A') }.
+
+Record D := {
+  D_A : A;
+  D_P : P D_A;
+  D_Q : Q D_A }.
+
+Local Coercion A'_A : A' >-> A.
+Local Coercion B_A' : B >-> A'.
+Local Coercion C_A' : C >-> A'.
+Local Coercion D_A : D >-> A.
+Local Coercion D_B (d : D) : B false :=
+  Build_B false (Build_A' false (D_A d)) (D_P d).
+Local Coercion D_C (d : D) : C true :=
+  Build_C true (Build_A' true (D_A d)) (D_Q d).
+
+Print Graph.
+
+End test4.
+End test4.
diff --git a/test-suite/ssr/elim_noquant.v b/test-suite/ssr/elim_noquant.v
new file mode 100644
index 0000000000..e6662203e9
--- /dev/null
+++ b/test-suite/ssr/elim_noquant.v
@@ -0,0 +1,29 @@
+Require Import ssreflect.
+
+
+Axiom app : forall T, list T -> list T -> list T.
+Arguments app {_}.
+Infix "++" := app.
+
+Lemma test (aT rT : Type)
+           (pmap : (aT -> option rT) -> list aT -> list rT)
+           (perm_eq : list rT -> list rT -> Prop)
+           (f : aT -> option rT)
+           (g : rT -> aT)
+           (s t : list aT)
+           (E : forall T : list aT -> Type,
+               (forall s1 s2 s3 : list aT,
+                  T (s1 ++ s2 ++ s3) -> T (s2 ++ s1 ++ s3)) ->
+                 T s -> T t) :
+        perm_eq (pmap f s) (pmap f t).
+Proof.
+elim/E: (t).
+Admitted.
+
+
+Lemma test2 (a b : nat) : a = b -> b = 1.
+Proof.
+elim.
+match goal with |- a = 1 => idtac end.
+Admitted.
+
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 3d97f27b16..31fed98952 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -137,3 +137,12 @@ Module WithIndex.
   Monomorphic Constraint i < j.
   Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
 End WithIndex.
+
+Module CumulApp.
+
+  (* i is covariant here, and we have one parameter *)
+  Inductive foo@{i} (A : nat) : Type@{i+1} := mkfoo (B : Type@{i}).
+
+  Definition bar@{i j|i<=j} := fun x : foo@{i} 0 => x : foo@{j} 0.
+
+End CumulApp.