Camltac
/
  • Getting started
    • Overview
    • Quickstart
    • Installation
  • A tour of Camltac
    • Running OCaml code
    • Defining new tactics
    • Quotations
    • Antiquotations
    • Pattern matching over terms
    • Pattern matching over goals
    • Using OCaml libraries and preprocessors
    • Interoperability with Ltac2
    • Using internal Rocq APIs
    • Going further
  • Tutorials
    • Writing a tactic with Camltac
      • Setting up a Camltac project
      • Searching for exact matches
      • Matching goals with variables
      • Importing the tactic in other files
      • Using the tactic from Ltac2
      • Conclusion
  • How-to guides
    • How to use Camltac with Dune
    • How to use Camltac with Makefiles
    • How to configure your editor
  • Reference
    • Commands
      • Camltac Run
      • Camltac Module
      • Camltac Load
      • Camltac Eval
      • Camltac Check
    • Quotations
    • Pattern matching
    • Comparison with Ltac2
    • Ltac2 APIs
      • Constant
      • Constr
        • Binder
        • Cast
        • Pretype
        • Relevance
        • Unsafe
      • Constructor
      • Control
      • Env
      • Fresh
        • Free
      • Ident
      • Ind
      • Message
      • Module
        • Field
      • Pattern
      • Proj
      • Rewrite
        • Strategy
      • Scheme
      • Std
        • Red
      • Syntax
        • Induction_arg
        • Induction_clause
      • TransparentState
      • Unification
  • Explanation
    • Why Camltac?
    • Camltac’s execution model
      • Parsing
      • Build directives
      • Compilation
      • Dynamic linking
      • Camltac’s runtime
  • Advanced topics
    • Using Rocq’s internal APIs

Additional links

  • Rocqshop 2026
  • Master's thesis
  1. Camltac /
  2. Explanation

Explanation#

  • Why Camltac?
  • Camltac’s execution model
Previous
Unification
Next
Why Camltac?

2026, Dario Halilovic (SYSTEMF @ EPFL)

Made with Sphinx and Shibuya theme.