14 files changed, 183 insertions, 106 deletions
diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v
index 1507fa4bf0..bd9bac37ef 100644
--- a/test-suite/bugs/closed/4717.v
+++ b/test-suite/bugs/closed/4717.v
@@ -19,8 +19,6 @@ Proof.
   omega.
 Qed.
 
-Require Import ZArith ROmega.
-
 Open Scope Z_scope.
 
 Definition Z' := Z.
@@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m,
 Proof.
   intros.
   omega.
-  Undo.
-  romega.
 Qed.
diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v
new file mode 100644
index 0000000000..c4b29a6354
--- /dev/null
+++ b/test-suite/bugs/closed/8215.v
@@ -0,0 +1,14 @@
+(* Check that instances for local definitions in evars have compatible body *)
+Goal False.
+Proof.
+  pose (n := 1).
+  evar (m:nat).
+  subst n.
+  pose (n := 0).
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clearbody n.
+  Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *)
+  clear n.
+  pose (n := 0+1).
+  Check ?m. (* Should be ok *)
+Abort.
diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v
new file mode 100644
index 0000000000..00aa66e701
--- /dev/null
+++ b/test-suite/bugs/closed/8532.v
@@ -0,0 +1,8 @@
+(* Checking Print Assumptions relatively to a bound module *)
+
+Module Type Typ.
+  Parameter Inline(10) t : Type.
+End Typ.
+Module  Terms_mod (SetVars : Typ).
+Print Assumptions SetVars.t.
+End Terms_mod.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 926114a1e1..f8f11d7cf6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E}
 (* E M N |=  *)
 
 foo is universe polymorphic
-foo@{Top.16 Top.17 Top.18} = 
-Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
-(* Top.16 Top.17 Top.18 |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Top.17+1,v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
 NonCumulative Inductive Empty@{E} : Type@{E} :=  
@@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v}
 (* v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{k}
+
+For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{u k}
+
+For inseccstr: Argument scope is [type_scope]
 inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -155,24 +163,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.51} -> Type@{axbar'.i}
+axfoo' : Type@{Top.58} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.51} -> Type@{axbar'.i}
+axbar' : Type@{Top.58} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index f806a9f4f7..9aebce1b9a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -122,8 +122,12 @@ Section SomeSec.
   Universe u.
   Definition insec@{v} := Type@{u} -> Type@{v}.
   Print insec.
+
+  Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
+  Print insecind.
 End SomeSec.
 Print insec.
+Print insecind.
 
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out
index 7326f137c2..8a00cd3fe5 100644
--- a/test-suite/output/ltac_missing_args.out
+++ b/test-suite/output/ltac_missing_args.out
@@ -1,25 +1,25 @@
 The command has indeed failed with message:
-The user-defined tactic "Top.foo" was not fully applied:
+The user-defined tactic "foo" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.bar" was not fully applied:
+The user-defined tactic "bar" was not fully applied:
 There are missing arguments for variables y and _,
 an argument was provided for variable x.
 The command has indeed failed with message:
-The user-defined tactic "Top.baz" was not fully applied:
+The user-defined tactic "baz" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.qux" was not fully applied:
+The user-defined tactic "qux" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.mydo" was not fully applied:
+The user-defined tactic "mydo" was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
@@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied:
 There is a missing argument for variable _,
 no arguments at all were provided.
 The command has indeed failed with message:
-The user-defined tactic "Top.rec" was not fully applied:
+The user-defined tactic "rec" was not fully applied:
 There is a missing argument for variable x,
 no arguments at all were provided.
 The command has indeed failed with message:
diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v
new file mode 100644
index 0000000000..422bb95fdf
--- /dev/null
+++ b/test-suite/ssr/ssrpattern.v
@@ -0,0 +1,7 @@
+Require Import ssrmatching.
+
+Goal forall n, match n with 0 => 0 | _ => 0 end = 0.
+Proof.
+  intro n.
+  ssrpattern (match _ with 0 => _ | S n' => _ end).
+Abort.
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index 0df3d5685d..a97afa7ff0 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -1,5 +1,7 @@
-
-Require Import ZArith ROmega.
+(* This file used to test the `romega` tactics.
+   In Coq 8.9 (end of 2018), these tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+Require Import ZArith Lia.
 
 (* Submitted by Xavier Urbain 18 Jan 2002 *)
 
@@ -7,14 +9,14 @@ Lemma lem1 :
  forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 Proof.
 intros x y.
-romega.
+lia.
 Qed.
 
 (* Proposed by Pierre Crégut *)
 
 Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
 intro.
- romega.
+ lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre *)
@@ -22,7 +24,7 @@ Qed.
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
@@ -32,7 +34,7 @@ Section A.
 Variable x y : Z.
 Hypothesis H : (x > y)%Z.
 Lemma lem4 : (x > y)%Z.
- romega.
+ lia.
 Qed.
 End A.
 
@@ -48,7 +50,7 @@ Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
 Hypothesis M : (H <= 2 * S)%Z.
 Hypothesis N : (S < H)%Z.
 Lemma lem5 : (H > 0)%Z.
- romega.
+ lia.
 Qed.
 End B.
 
@@ -56,11 +58,10 @@ End B.
 Lemma lem6 :
  forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
 intros.
- romega.
+ lia.
 Qed.
 
 (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
-Require Import Omega.
 Section C.
 Parameter g : forall m : nat, m <> 0 -> Prop.
 Parameter f : forall (m : nat) (H : m <> 0), g m H.
@@ -68,23 +69,21 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- romega with nat.
+ lia.
 Qed.
 End C.
 
 (* Problem of dependencies *)
-Require Import Omega.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 intros.
-romega with nat.
+lia.
 Qed.
 
 (* Bug that what caused by the use of intro_using in Omega *)
-Require Import Omega.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 intros.
-romega with nat.
+lia.
 Qed.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
@@ -92,5 +91,5 @@ Qed.
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m : nat, le n (plus n (mult n m)).
 Proof.
-intros; romega with nat.
+intros; lia.
 Qed.
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 3ddf6a40fb..7f69422ab3 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -1,25 +1,27 @@
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Open Scope Z_scope.
 
 (* Pierre L: examples gathered while debugging romega. *)
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
 
-Lemma test_romega_0 :
+Lemma test_lia_0 :
  forall m m',
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_0b :
+Lemma test_lia_0b :
  forall m m',
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros m m'.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_1 :
+Lemma test_lia_1 :
  forall (z z1 z2 : Z),
     z2 <= z1 ->
     z1 <= z2 ->
@@ -29,10 +31,10 @@ Lemma test_romega_1 :
     z >= 0.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_1b :
+Lemma test_lia_1b :
  forall (z z1 z2 : Z),
     z2 <= z1 ->
     z1 <= z2 ->
@@ -42,24 +44,24 @@ Lemma test_romega_1b :
     z >= 0.
 Proof.
 intros z z1 z2.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_2 : forall a b c:Z,
+Lemma test_lia_2 : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_2b : forall a b c:Z,
+Lemma test_lia_2b : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros a b c.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_3 : forall a b h hl hr ha hb,
+Lemma test_lia_3 : forall a b h hl hr ha hb,
  0 <= ha - hl <= 1 ->
  -2 <= hl - hr <= 2 ->
  h =b+1 ->
@@ -70,10 +72,10 @@ Lemma test_romega_3 : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_3b : forall a b h hl hr ha hb,
+Lemma test_lia_3b : forall a b h hl hr ha hb,
  0 <= ha - hl <= 1 ->
  -2 <= hl - hr <= 2 ->
  h =b+1 ->
@@ -84,79 +86,79 @@ Lemma test_romega_3b : forall a b h hl hr ha hb,
  0 <= hb - h <= 1.
 Proof.
 intros a b h hl hr ha hb.
-romega.
+lia.
 Qed.
 
 
-Lemma test_romega_4 : forall hr ha,
+Lemma test_lia_4 : forall hr ha,
  ha = 0 ->
  (ha = 0 -> hr =0) ->
  hr = 0.
 Proof.
 intros hr ha.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_5 : forall hr ha,
+Lemma test_lia_5 : forall hr ha,
  ha = 0 ->
  (~ha = 0 \/ hr =0) ->
  hr = 0.
 Proof.
 intros hr ha.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Lemma test_lia_6 : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Lemma test_lia_6b : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros z.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_7 : forall z,
+Lemma test_lia_7 : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_7b : forall z,
+Lemma test_lia_7b : forall z,
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Magaud BZ#240 *)
 
-Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Lemma test_lia_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
-Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+Lemma test_lia_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
 Proof.
 intros x y.
-romega.
+lia.
 Qed.
 
 (* Besson BZ#1298 *)
 
-Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+Lemma test_lia9 : forall z z':Z, z<>z' -> z'=z -> False.
 Proof.
 intros.
-romega.
+lia.
 Qed.
 
 (* Letouzey, May 2017 *)
 
-Lemma test_romega10 : forall x a a' b b',
+Lemma test_lia10 : forall x a a' b b',
  a' <= b ->
  a <= b' ->
  b < b' ->
@@ -164,5 +166,5 @@ Lemma test_romega10 : forall x a a' b b',
  a <= x < b' <-> a <= x < b \/ a' <= x < b'.
 Proof.
  intros.
- romega.
+ lia.
 Qed.
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index 43eda67ea3..e3b090699d 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -1,4 +1,6 @@
-Require Import ZArith ROmega.
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+Require Import ZArith Lia.
 
 (* Submitted by Yegor Bryukhov (BZ#922) *)
 
@@ -13,7 +15,7 @@ forall v1 v2 v5 : Z,
 0 < v2 ->
 4*v2 <> 5*v1.
 intros.
-romega.
+lia.
 Qed.
 
 
@@ -37,5 +39,5 @@ forall v1 v2 v3 v4 v5 : Z,
 ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 -> False.
 intros.
-romega.
+lia.
 Qed.
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
index fd4ff260b5..ef9cb17b4b 100644
--- a/test-suite/success/ROmega3.v
+++ b/test-suite/success/ROmega3.v
@@ -1,10 +1,14 @@
 
-Require Import ZArith ROmega.
+Require Import ZArith Lia.
 Local Open Scope Z_scope.
 
 (** Benchmark provided by Chantal Keller, that romega used to
     solve far too slowly (compared to omega or lia). *)
 
+(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
+
+
 Parameter v4 : Z.
 Parameter v3 : Z.
 Parameter o4 : Z.
@@ -27,5 +31,5 @@ Lemma lemma_5833 :
       (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
          (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
 Proof.
-Timeout 1 romega. (* should take a few milliseconds, not seconds *)
+Timeout 1 lia. (* should take a few milliseconds, not seconds *)
 Timeout 1 Qed. (* ditto *)
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index fa659273e1..6ca32f450f 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -1,127 +1,123 @@
-Require Import ZArith Nnat ROmega.
+Require Import ZArith Nnat Lia.
 Open Scope Z_scope.
 
 (** Test of the zify preprocessor for (R)Omega *)
+(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
+   The tests in this file remain but now call the `lia` tactic. *)
 
 (* More details in file PreOmega.v
-
-   (r)omega with Z        : starts with zify_op
-   (r)omega with nat      : starts with zify_nat
-   (r)omega with positive : starts with zify_positive
-   (r)omega with N        : starts with uses zify_N
-   (r)omega with *        : starts zify (a saturation of the others)
 *)
 
 (* zify_op *)
 
 Goal forall a:Z, Z.max a a = a.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
-intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
+intuition; subst; lia. (* pure multiplication: omega alone can't do it *)
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_nat *)
 
 Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 (* 2000 instead of 200: works, but quite slow *)
 
 Goal forall m: nat, (m*m>=0)%nat.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_positive *)
 
 Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m: positive, (m*m>=1)%positive.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* zify_N *)
 
 Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m<1)%N -> (m=0)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 Goal forall m:N, (m*m>=0)%N.
 intros.
-romega with *.
+lia.
 Qed.
 
 (* mix of datatypes *)
 
 Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
-romega with *.
+lia.
 Qed.
 
 
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
index 83fb3d0c8e..241d4eb200 100644
--- a/test-suite/success/attribute-syntax.v
+++ b/test-suite/success/attribute-syntax.v
@@ -1,4 +1,4 @@
-From Coq Require Program.
+From Coq Require Program.Wf.
 
 Section Scope.
 
@@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _.
 
 #[deprecated(since="8.9.0")]
 Ltac foo := foo.
+
+Module M.
+  #[local] #[polymorphic] Definition zed := Type.
+
+  #[local, polymorphic] Definition kats := Type.
+End M.
+Check M.zed@{_}.
+Fail Check zed.
+Check M.kats@{_}.
+Fail Check kats.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 4404ff3f16..448febed25 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -377,3 +377,30 @@ f y true.
 Abort.
 
 End LtacNames.
+
+(* Test binding of the name of existential variables in Ltac *)
+
+Module EvarNames.
+
+Ltac pick x := eexists ?[x].
+Goal exists y, y = 0.
+pick foo.
+[foo]:exact 0.
+auto.
+Qed.
+
+Ltac goal x := refine ?[x].
+
+Goal forall n, n + 0 = n.
+Proof.
+  induction n; [ goal Base | goal Rec ].
+  [Base]: {
+    easy.
+  }
+  [Rec]: {
+    simpl.
+    now f_equal.
+  }
+Qed.
+
+End EvarNames.