plugins/ltac · coq · Tangled

forked from coq/coq

coq plugins ltac

56 files

Pierre Roux · [ssreflect] Accept `tac; [tac|...|tac] => intro` syntax · 1mo ago

Implement `{| foo with fields |}` for terms

Add source location for Add Morphism, Add Relation

coretactics.mlg

wit_tactic top type is tacvalue

coretactics.mli

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

Remove compat coq-core libraries (not executables)

wit_tactic top type is tacvalue

wit_tactic top type is tacvalue

extratactics.mlg

Abstract away the Summary reference type.

extratactics.mli

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

Move the Ftactic module to the Ltac plugin.

Move the Ftactic module to the Ltac plugin.

Introduce PolyFlags to gather flags for polymorphic defs

Fix parsing warnings in test-suite

Avoid declaring a parsing rule for head_of_constr

Rename the Pcoq module into Procq.

rename package coq-core -> rocq-runtime

Enable warning 70 (missing mli), add mli files

[ssreflect] Accept `tac; [tac|...|tac] => intro` syntax

[ssreflect] Accept `tac; [tac|...|tac] => intro` syntax

Use levels instead of separate entries for rewrite strategies

Move Geninterp.interp_sign to ltac plugin

Change the semantics of the deprecated intropattern genarg.

Rename the Pcoq module into Procq.

Rename is_section_variable' -> is_section_variable_env

add is_section_var tactic

Use variable status to decide if a variable is section variable

Introduce PolyFlags to gather flags for polymorphic defs

[ssreflect] Accept `tac; [tac|...|tac] => intro` syntax

[ssreflect] Accept `tac; [tac|...|tac] => intro` syntax

Abstract away the Summary reference type.

[ssreflect] Rename SSR Loaded to SSRRewriteLoaded

profile_ltac_tactics.mlg

rename package coq-core -> rocq-runtime

profile_ltac_tactics.mli

Enable warning 70 (missing mli), add mli files

rewriteStratAst.ml

Move rewrite strat asts to ltac1 plugin

rewriteStratAst.mli

Move rewrite strat asts to ltac1 plugin

Hide definition of tacvalue in tacinterp

Hide definition of tacvalue in tacinterp

QGlobal is not QVar

wit_tactic top type is tacvalue

Merge PR #22329: [ltac] accept constrN, open_constrN and uconstrN as a tactic argument

Removed unused deprecation arguments in tacentries

Abstract away the Summary reference type.

Make it possible to warn when interning a TACTIC EXTEND + use for ssr rewrite

Move rewrite strat asts to ltac1 plugin

Make it possible to warn when interning a TACTIC EXTEND + use for ssr rewrite

Check universes are declared in constr inside tactics

interp_nat_or_var use variable loc for error

[ssreflect] Deprecate rewrite

Stop using genarg for constr syntax extension

Make the Genredexpr.red_expr_gen type open-ended.

tactic_debug.ml

Deprecate Tacmach.project.

tactic_debug.mli

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

tactic_matching.ml

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

tactic_matching.mli

More type enforced "instantiation" of constr patterns

wit_tactic top type is tacvalue

Ltac as a plugin.