Merge branch 'v8.6'

4 files changed, 313 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 0000000000..14af2d91df
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,45 @@
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Goal True.
+  idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
+Abort.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v
new file mode 100644
index 0000000000..3ded4dd304
--- /dev/null
+++ b/test-suite/bugs/closed/5093.v
@@ -0,0 +1,11 @@
+Axiom P : nat -> Prop.
+Axiom PS : forall n, P n -> P (S n).
+Axiom P0 : P 0.
+
+Hint Resolve PS : foobar.
+Hint Resolve P0 : foobar.
+
+Goal P 100.
+Proof.
+Fail typeclasses eauto 100 with foobar.
+typeclasses eauto 101 with foobar.
diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v
new file mode 100644
index 0000000000..20a537ab3c
--- /dev/null
+++ b/test-suite/bugs/closed/5096.v
@@ -0,0 +1,219 @@
+Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
+
+Set Asymmetric Patterns.
+
+Notation eta x := (fst x, snd x).
+
+Inductive expr {var : Type} : Type :=
+| Const : expr
+| LetIn : expr -> (var -> expr) -> expr.
+
+Definition Expr := forall var, @expr var.
+
+Fixpoint count_binders (e : @expr unit) : nat :=
+match e with
+| LetIn _ eC => 1 + @count_binders (eC tt)
+| _ => 0
+end.
+
+Definition CountBinders (e : Expr) : nat := count_binders (e _).
+
+Class Context (Name : Type) (var : Type) :=
+  { ContextT : Type;
+    extendb : ContextT -> Name -> var -> ContextT;
+    empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _}, {_ _} _.
+Arguments extendb {_ _ _} _ _ _.
+Arguments empty {_ _ _}.
+
+Module Export Named.
+Inductive expr Name : Type :=
+| Const : expr Name
+| LetIn : Name -> expr Name -> expr Name -> expr Name.
+End Named.
+
+Global Arguments Const {_}.
+Global Arguments LetIn {_} _ _ _.
+
+Definition split_onames {Name : Type} (ls : list (option Name))
+  : option (Name) * list (option Name)
+  := match ls with
+          | cons n ls'
+            => (n, ls')
+          | nil => (None, nil)
+     end.
+
+Section internal.
+  Context (InName OutName : Type)
+          {InContext : Context InName (OutName)}
+          {ReverseContext : Context OutName (InName)}
+          (InName_beq : InName -> InName -> bool).
+
+  Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+           (e : expr InName) (new_names : list (option OutName))
+    : option (expr OutName)
+    := match e in Named.expr _ return option (expr _) with
+       | Const => Some Const
+       | LetIn n ex eC
+         => let '(n', new_names') := eta (split_onames new_names) in
+            match n', @register_reassign ctxi ctxr ex nil with
+            | Some n', Some x
+              => let ctxi := @extendb _ _ _ ctxi n n' in
+                 let ctxr := @extendb _ _ _ ctxr n' n in
+                 option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
+            | None, Some x
+              => let ctxi := ctxi in
+                 @register_reassign ctxi ctxr eC new_names'
+            | _, None => None
+            end
+       end.
+
+End internal.
+
+Global Instance pos_context (var : Type) : Context positive var
+  := { ContextT := PositiveMap.t var;
+       extendb ctx key v := PositiveMap.add key v ctx;
+       empty := PositiveMap.empty _ }.
+
+Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
+
+Section language5.
+  Context (Name : Type).
+
+  Local Notation expr := (@Top.expr Name).
+  Local Notation nexpr := (@Named.expr Name).
+
+  Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
+    : option (nexpr)
+    := match e in @Top.expr _ return option (nexpr) with
+       | Top.Const => Some Named.Const
+       | Top.LetIn ex eC
+         => match @ocompile ex nil, split_onames ls with
+            | Some x, (Some n, ls')%core
+              => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
+            | _, _ => None
+            end
+       end.
+
+  Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
+End language5.
+
+Global Arguments compile {_} e ls.
+
+Fixpoint merge_liveness (ls1 ls2 : list unit) :=
+  match ls1, ls2 with
+  | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
+  | nil, ls | ls, nil => ls
+  end.
+
+Section internal1.
+  Context (Name : Type)
+          (OutName : Type)
+          {Context : Context Name (list unit)}.
+
+  Definition compute_livenessf_step
+             (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
+             (ctx : Context)
+             (e : expr Name) (prefix : list unit)
+    : list unit
+    := match e with
+       | Const => prefix
+       | LetIn n ex eC
+         => let lx := @compute_livenessf ctx ex prefix in
+            let lx := merge_liveness lx (prefix ++ repeat tt 1) in
+            let ctx := @extendb _ _ _ ctx n (lx) in
+            @compute_livenessf ctx eC (prefix ++ repeat tt 1)
+       end.
+
+  Fixpoint compute_liveness ctx e prefix
+    := @compute_livenessf_step (@compute_liveness) ctx e prefix.
+
+  Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
+    : list (option OutName)
+    := match ls with
+       | nil => nil
+       | cons live xs
+         => match lsn with
+            | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
+            | nil => def :: @insert_dead_names_gen def xs nil
+            end
+       end.
+  Definition insert_dead_names def (e : expr Name)
+    := insert_dead_names_gen def (compute_liveness empty e nil).
+End internal1.
+
+Global Arguments insert_dead_names {_ _ _} def e lsn.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+
+Section language7.
+  Context {Context : Context unit (positive)}.
+
+  Local Notation nexpr := (@Named.expr unit).
+
+  Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
+    : option (nexpr)
+    := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
+       match e with
+       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
+                          (fun names => register_reassign empty empty e names)
+       | None => None
+       end.
+End language7.
+
+Global Arguments CompileAndEliminateDeadCode {_} e ls.
+
+Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
+  := {| ContextT := Ctx;
+        extendb ctx n v := extendb ctx (f n) v;
+        empty := empty |}.
+
+Definition Register := Datatypes.unit.
+
+Global Instance RegisterContext {var : Type} : Context Register var
+  := ContextOn (fun _ => 1%positive) (pos_context var).
+
+Definition syntax := Named.expr Register.
+
+Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
+  := match res return match res with None => _ | _ => _ end with
+     | Some v => v
+     | None => I
+     end.
+
+Definition dummy_registers (n : nat) : list Register
+  := List.map (fun _ => tt) (seq 0 n).
+Definition DefaultRegisters (e : Expr) : list Register
+  := dummy_registers (CountBinders e).
+
+Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
+
+Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@Top.Const var).
+
+Definition compiled_syntax : Expr := fun (var : Type) =>
+(
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+ @Top.Const var).
+
+Definition v :=
+  Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
+
+Timeout 2 Eval vm_compute in v.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cfd..356a67efec 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.