Learn
Platform
Packages
Community
Consortium
News

Learn
Platform
Packages
Community
Consortium
News
Get started

Core Library
▾

Table of contents Index

Library Ltac2.Compat.Coq819

Require Ltac2.Init.

#[export] Unset Ltac2 Typed Notations.

Footer

Interactive Theorem Prover

Zulip GitHub Discourse Mastodon RSS

GitHub branch and commit.

About Rocq

Changelog
Releases
Industrial Users
Academic Users
History
Why Rocq?
Roadmap

Resources

Install Rocq
Get Started
Documentation
Reference Manual
Standard Library
Books
Exercises
Papers
Logo

Ecosystem

Platform
Packages
Community
Consortium
Events
Rocq Planet
Jobs

Policies

Rocq Team
Governance
Privacy
Code of Conduct