10 files changed, 198 insertions, 1 deletions
diff --git a/test-suite/output/bug_10803.out b/test-suite/output/bug_10803.out
new file mode 100644
index 0000000000..04d190a5d1
--- /dev/null
+++ b/test-suite/output/bug_10803.out
@@ -0,0 +1,10 @@
+a !
+     : Foo
+where
+?y : [ |- nat]
+a !
+     : Foo
+a
+     : Foo -> Foo
+a !
+     : Foo
diff --git a/test-suite/output/bug_10803.v b/test-suite/output/bug_10803.v
new file mode 100644
index 0000000000..1f2027d061
--- /dev/null
+++ b/test-suite/output/bug_10803.v
@@ -0,0 +1,14 @@
+Inductive Foo := foo.
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Bind Scope foo_scope with Foo.
+Notation "'!'" := foo : foo_scope.
+Definition of_foo {x : nat} {y : nat} (f : Foo) := f.
+Notation a := (@of_foo O).
+Notation b := (@a).
+Check a !.
+Check @a O !.
+Check @b O.
+Check @b O !. (* was failing *)
+(* All are printed "a !", without making explicit the "0", which is
+   incidentally disputable *)
diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
new file mode 100644
index 0000000000..2bd7d67535
--- /dev/null
+++ b/test-suite/output/bug_13004.out
@@ -0,0 +1,2 @@
+Ltac bug_13004.t := ltac2:(print (of_string "hi"))
+Ltac bug_13004.u := ident:(H)
diff --git a/test-suite/output/bug_13004.v b/test-suite/output/bug_13004.v
new file mode 100644
index 0000000000..bf4a8285d0
--- /dev/null
+++ b/test-suite/output/bug_13004.v
@@ -0,0 +1,7 @@
+Require Import Ltac2.Ltac2 Ltac2.Message.
+
+Ltac t := ltac2:(print (of_string "hi")).
+Ltac u := ident:(H).
+
+Print t.
+Print u.
diff --git a/test-suite/output/bug_13018.out b/test-suite/output/bug_13018.out
new file mode 100644
index 0000000000..2f60409e23
--- /dev/null
+++ b/test-suite/output/bug_13018.out
@@ -0,0 +1,14 @@
+gargs:( (!) )
+     : list nat
+gargs:( (!, !, !) )
+     : list nat
+OnlyGargs[ (!) ]
+     : list nat
+gargs999:( (!) )
+     : list nat
+gargs999:( (!, !, !) )
+     : list nat
+OnlyGargs[ (!) ]
+     : list nat
+OnlyGargs999[ (!) ]
+     : list nat
diff --git a/test-suite/output/bug_13018.v b/test-suite/output/bug_13018.v
new file mode 100644
index 0000000000..3fb8b7f905
--- /dev/null
+++ b/test-suite/output/bug_13018.v
@@ -0,0 +1,30 @@
+Undelimit Scope list_scope.
+Declare Custom Entry gnat.
+Declare Custom Entry gargs.
+
+Notation "!" := 42 (in custom gnat).
+Notation "gargs:( e  )" := e (e custom gargs).
+Notation "( x )" := (cons x (@nil nat)) (in custom gargs, x custom gnat).
+Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
+  (in custom gargs, x custom gnat, y custom gnat, z custom gnat).
+
+Check gargs:( (!) ). (* cons 42 nil *)
+Check gargs:( (!, !, !) ). (* cons 42 (42 :: 42 :: nil) *)
+
+Definition OnlyGargs {T} (x:T) := x.
+Notation "OnlyGargs[ x  ]" := (OnlyGargs x) (at level 10, x custom gargs).
+Check OnlyGargs[ (!) ]. (* OnlyGargs[ cons 42 nil] *)
+
+Declare Custom Entry gargs999.
+Notation "gargs999:( e  )" := e (e custom gargs999 at level 999).
+Notation "( x )" := (cons x (@nil nat)) (in custom gargs999, x custom gnat at level 999).
+Notation "( x , y , .. , z )" := (cons x (cons y .. (cons z nil) ..))
+  (in custom gargs999, x custom gnat at level 999, y custom gnat at level 999, z custom gnat at level 999).
+
+Check gargs999:( (!) ). (* gargs999:( (!)) *)
+Check gargs999:( (!, !, !) ). (* gargs999:( (!, !, !)) *)
+Check OnlyGargs[ (!) ]. (* OnlyGargs[ gargs999:( (!))] *)
+
+Definition OnlyGargs999 {T} (x:T) := x.
+Notation "OnlyGargs999[ x  ]" := (OnlyGargs999 x) (at level 10, x custom gargs999 at level 999).
+Check OnlyGargs999[ (!) ]. (* OnlyGargs999[ (!)] *)
diff --git a/test-suite/output/bug_9403.out b/test-suite/output/bug_9403.out
new file mode 100644
index 0000000000..850760d5ed
--- /dev/null
+++ b/test-suite/output/bug_9403.out
@@ -0,0 +1,6 @@
+1 subgoal
+  
+  X : tele
+  α, β, γ1, γ2 : X → Prop
+  ============================
+  accessor α β γ1 → accessor α β (λ.. x : X, γ1 x ∨ γ2 x)
diff --git a/test-suite/output/bug_9403.v b/test-suite/output/bug_9403.v
new file mode 100644
index 0000000000..b915e7fbce
--- /dev/null
+++ b/test-suite/output/bug_9403.v
@@ -0,0 +1,99 @@
+(* Uselessly long but why not *)
+
+From Coq Require Export Utf8.
+
+Local Set Universe Polymorphism.
+
+Module tele.
+(** Telescopes *)
+Inductive tele : Type :=
+  | TeleO : tele
+  | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+  match TT with
+  | TeleO => T
+  | TeleS b => ∀ x, tele_fun (b x) T
+  end.
+
+Notation "TT -t> A" :=
+  (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** An eliminator for elements of [tele_fun].
+    We use a [fix] because, for some reason, that makes stuff print nicer
+    in the proofs in iris:bi/lib/telescopes.v *)
+Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y)
+  : (TT -t> X) → Y :=
+  (fix rec {TT} : (TT -t> X) → Y :=
+     match TT as TT return (TT -t> X) → Y with
+     | TeleO => λ x : X, base x
+     | TeleS b => λ f, step (λ x, rec (f x))
+     end) TT.
+Arguments tele_fold {_ _ !_} _ _ _ /.
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+  takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+  λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+     match a in tele_arg TT return (TT -t> T) → T with
+     | TargO => λ t : T, t
+     | TargS x a => λ f, rec a (f x)
+     end) TT a f.
+Arguments tele_app {!_ _} _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Local Coercion tele_app : tele_fun >-> Funclass.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+  match TT as TT return (TT → U) → TT -t> U with
+  | TeleO => λ F, F TargO
+  | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+                  tele_bind (λ a, F (TargS x a))
+  end.
+Arguments tele_bind {_ !_} _ /.
+
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
+   binder so that, after simplifying, this matches the way we typically write
+   notations involving telescopes. *)
+Notation "t $ r" := (t r)
+  (at level 65, right associativity, only parsing).
+Notation "'λ..' x .. y , e" :=
+  (tele_app $ tele_bind (λ x, .. (tele_app $ tele_bind (λ y, e)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+   format "'[  ' 'λ..'  x  ..  y ']' ,  e").
+
+(** Telescopic quantifiers *)
+Definition texist {TT : tele} (Ψ : TT → Prop) : Prop :=
+  tele_fold ex (λ x, x) (tele_bind Ψ).
+Arguments texist {!_} _ /.
+
+Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. ))
+  (at level 200, x binder, y binder, right associativity,
+  format "∃..  x  ..  y ,  P").
+End tele.
+Import tele.
+
+(* This is like Iris' accessors, but in Prop.  Just to play with telescopes. *)
+Definition accessor {X : tele} (α β γ : X → Prop) : Prop :=
+  ∃.. x, α x ∧ (β x → γ x).
+
+(* Working with abstract telescopes. *)
+Section tests.
+Context {X : tele}.
+Implicit Types α β γ : X → Prop.
+
+Lemma acc_mono_disj α β γ1 γ2 :
+  accessor α β γ1 → accessor α β (λ.. x, γ1 x ∨ γ2 x).
+Show.
+Abort.
+End tests.
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
index 58931c4b82..5f88ec2e41 100644
--- a/test-suite/output/print_ltac.out
+++ b/test-suite/output/print_ltac.out
@@ -4,7 +4,7 @@ Ltac t2 := let x := string:("my tactic") in
            x
 Ltac t3 := idtacstr "my tactic"
 Ltac t4 x := match x with
-             | ?A => (A, A)
+             | ?A => constr:((A, A))
              end
 The command has indeed failed with message:
 idnat is bound to a notation that does not denote a reference.
diff --git a/test-suite/success/eqtacticsnois.v b/test-suite/success/eqtacticsnois.v
new file mode 100644
index 0000000000..7869532c67
--- /dev/null
+++ b/test-suite/success/eqtacticsnois.v
@@ -0,0 +1,15 @@
+(* coq-prog-args: ("-nois") *)
+
+Inductive eq {A : Type} (x : A) : forall a:A, Prop :=  eq_refl : eq x x.
+
+Axiom sym : forall A (x y : A) (_ : eq x y), eq y x.
+Require Import Ltac.
+
+Register eq as core.eq.type.
+Register sym as core.eq.sym.
+
+Goal forall A (x y:A) (_ : forall z, eq y z), eq x x.
+intros * H. replace x with y.
+- reflexivity.
+- apply H.
+Qed.