plugins/ltac2 · coq · Tangled

forked from coq/coq

coq plugins ltac2

46 files

Pierre-Marie Pédrot · Use the now correct set and maps Names APIs. · 1mo ago

Remove compat coq-core libraries (not executables)

Use Grammar Extend for ltac2 constr grammar extensions

Move code about ltac2 notations to new file tac2syn from Tac2entries

Redesign Goptions API

Update the OCaml headers to reflect the fact Coq is now Rocq.

Use the now correct set and maps Names APIs.

Use the now correct set and maps Names APIs.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Update the OCaml headers to reflect the fact Coq is now Rocq.

Ltac2 Abbreviations typecheck at declaration time

tac2entries.mli

Ltac2 scoped notations (basic features)

Abstract away the Summary reference type.

Ltac2 Abbreviations typecheck at declaration time

Renaming in ML APIs about ltac2 abbreviations: alias -> abbrev

tac2externals.ml

Update the OCaml headers to reflect the fact Coq is now Rocq.

tac2externals.mli

Update the OCaml headers to reflect the fact Coq is now Rocq.

Ltac2 move format type def out of Tac2print

Ltac2 move format type def out of Tac2print

tac2extravals.ml

Add a deprecated option to restore the previous abstract behaviour.

tac2extravals.mli

Split quotation registrations and syntactic classes off from tac2core

Replace string scheme kinds with abstract type in Ltac2 API

Replace string scheme kinds with abstract type in Ltac2 API

Ltac2 Abbreviations typecheck at declaration time

Stop exposing Tac2intern.globalize

Names: move set/map modules `KNset` -> `KerName.Set` etc

Update the OCaml headers to reflect the fact Coq is now Rocq.

More type enforced "instantiation" of constr patterns

Update the OCaml headers to reflect the fact Coq is now Rocq.

Renaming in ML APIs about ltac2 abbreviations: alias -> abbrev

Merge PR #20498: Ltac2 add `%A` and `%m` format specifiers taking unthunked printer and message respectively

Stop saying "scope" when talking about ltac2 syntactic classes

Ltac2 module inspection API

Ltac2: provide user API for printing errors

Add Ltac2.Std.autorewrite_backward

Update the OCaml headers to reflect the fact Coq is now Rocq.

Renaming in ML APIs about ltac2 abbreviations: alias -> abbrev

Move code about mod subst from tac2intern to new file tac2subst

Abstract away the Summary reference type.

Ltac2 scoped notations (basic features)

Improve backwards compatibility by making `forward` optional

tac2tactics.mli

Improve backwards compatibility by making `forward` optional

Add ltac2 type for term conversions (`Red.t`) and make reduction tacs use it

tac2typing_env.ml

remove unused argument in ltac2 type normalization

tac2typing_env.mli

Ltac2 scoped notations (basic features)

Update the OCaml headers to reflect the fact Coq is now Rocq.

Rocqify some comments and description messages in plugins/.