-
Notifications
You must be signed in to change notification settings - Fork 22
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
- Status: Open.#118 In rocq-prover/platform-docs;
Tutorial on Coercions
WishWish for Tutorial or How-to guidesWish for Tutorial or How-to guidesStatus: Open.#117 In rocq-prover/platform-docs;- Status: Open.#108 In rocq-prover/platform-docs;
Improve tuto Equations wf: compute with wf and opaque proof
documentationImprovements or additions to documentationImprovements or additions to documentationImprovementsImprovementsImprovementsStatus: Open.#107 In rocq-prover/platform-docs;- Status: Open.#106 In rocq-prover/platform-docs;
Ltac2: Tuto Ltac2 for Ltac1 users
documentationImprovements or additions to documentationImprovements or additions to documentationWishWish for Tutorial or How-to guidesWish for Tutorial or How-to guidesStatus: Open.#103 In rocq-prover/platform-docs;Tuto Implicit Arguments
documentationImprovements or additions to documentationImprovements or additions to documentationWishWish for Tutorial or How-to guidesWish for Tutorial or How-to guidesStatus: Open.#102 In rocq-prover/platform-docs;Ltac2: Write a tuto about writing scripts
documentationImprovements or additions to documentationImprovements or additions to documentationWishWish for Tutorial or How-to guidesWish for Tutorial or How-to guidesStatus: Open.#100 In rocq-prover/platform-docs;Ltac2: Adapt tuto chaining tactics to Ltac1
documentationImprovements or additions to documentationImprovements or additions to documentationWishWish for Tutorial or How-to guidesWish for Tutorial or How-to guidesStatus: Open.#99 In rocq-prover/platform-docs;Ltac2: How to write a reflection tactic
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#98 In rocq-prover/platform-docs;Ltac2: Intro to Ltac2
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#97 In rocq-prover/platform-docs;Ltac2: Write a tuto on Notations
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#95 In rocq-prover/platform-docs;