plugins/ssr · coq · Tangled

forked from coq/coq

coq plugins ssr

26 files

Matthieu Sozeau · ssr: replace universe state unions by set_ustate when extending · 2w ago

Remove compat coq-core libraries (not executables)

Move Geninterp.interp_sign to ltac plugin

ssr: replace universe state unions by set_ustate when extending

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

ssr: replace universe state unions by set_ustate when extending

[ssreflect] Use ‗ instead of _ for reserved identifiers

ssr: replace universe state unions by set_ustate when extending

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

Fix handling of polymorphic universes in ssr matching

ssrequality.mli

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

Abstract away the Summary reference type.

wit_tactic top type is tacvalue

ssr: replace universe state unions by set_ustate when extending

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

Merge PR #22545: Implement deep %scope in Arguments

[ssreflect] Use tactic name 'rw' instead of 'rewrite'

Pass printing flags functionally in constr printers

ssrprinters.mli

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

[ssreflect] Use tactic name 'rw' instead of 'rewrite'

[ssreflect] Use tactic name 'rw' instead of 'rewrite'

ssrtacticals.ml

Small clean up around pf_ids_of_hyps in ssr tactics.

ssrtacticals.mli

wit_tactic top type is tacvalue

Add "if <term> is <pattern> then _ else _" syntax

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

Abstract away the Summary reference type.

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