Camltac Documentation

Camltac is an OCaml plugin for Rocq that lets you run OCaml code within Rocq scripts. Camltac makes it possible to define OCaml meta-programs and tactics, and run them in the current Rocq state without the friction and boilerplate of setting up a plugin.

• Getting started
  • Overview
  • Quickstart
  • Installation
• A tour of Camltac
• Tutorials
  • Writing a tactic with Camltac
• How-to guides
  • How to use Camltac with Dune
  • How to use Camltac with Makefiles
  • How to configure your editor
• Reference
  • Commands
  • Quotations
  • Pattern matching
  • Comparison with Ltac2
  • Ltac2 APIs
• Explanation
  • Why Camltac?
  • Camltac’s execution model
• Advanced topics
  • Using Rocq’s internal APIs