Jason Gross

- [ ] Added / updated **test-suite**. (is this needed here, since we're just exposing unerlying ml primitives?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (is...

- [ ] Added / updated **test-suite** (do we need it?) - [x] Added **changelog**. - [ ] Added / updated **documentation**. (do we need it?)

Ltac2 doc does not explain why `Control.refine` takes a thunk

1

#### Description of the problem In particular it's not clear what the difference is between `let x := f () in Control.refine (fun () => x)` and `Control.refine f`. (And...

Ltac2 should provide datatypes for hash sets and hash maps

3

#### Description of the problem I'd like to have hash maps and hash sets where where keys (for map) / values (for sets) are the following types: - `ident` -...

Ltac2 precedence of field access is not consistent with Gallina

2

#### Description of the problem In Gallina, `foo bar.(baz)` means `foo (bar.(baz))`. In Ltac2, it seems to mean `(foo bar).(baz)`. #### Coq Version 8.15

coqtop dies with "Fatal error: exception Not_found" when Ltac Backtrace is set and the backtrace references a constant which no longer exists

1

#### Description of the problem Finished failing transaction in 18.917 secs (18.809u,0.108s) (failure) Fatal error: exception Not_found Raised at Int.Map.find in [file "clib/int.ml", line 39](https://github.com/coq/coq/blob/V8.15.0/clib/int.ml#L39), characters 14-29 Called from HMap.Make.find...

`ltac2:(...)` in nested notations handles variable names incorrectly

1

#### Description of the problem This should work: ```coq Require Import Ltac2.Ltac2. Require Import Ltac2.Printf. Notation foo1 x := (ltac:(idtac x; exact I)) (only parsing). Notation bar1 y := (foo1...

Print Ltac2 Type

4

I'd like to be able to write `Print Ltac2 Type exn`

Ltac2 stack traces

7

#### Description of the problem I'd like to have a global setting that enables stack trace printing for Ltac2 errors. There should also be some support within the language for...

`open import Agda.Primitive using (Set) public` misbehaves in modules with arguments

3

```agda module foo where module A where open import Agda.Primitive using (Set; Setω; Level; lzero; lsuc; _⊔_) public A : ∀ l -> Set (lsuc l) A l = Set...