Commands#

General syntax#

OCaml code#

ocaml::=ocaml:open-delim ocaml-code close-delimopen-delim::=(+|[+|{+close-delim::=)+|]+|}+

The code must be closed by as many closing delimiters as there were opening ones, of the matching kind. For example, ocaml:(code), ocaml:[[code]] and ocaml:{{{code}}} are all valid.

Note

In general, you should prefer ocaml:{{code}}, since Rocq treats :{{ as a special case that does not end parsing on ..

Attributes#

attributes::=#[ attribute+, ]attribute::=localglobalexport|libraries( package+, )|ppx( package+, )|compiler( compiler-flag+, )

Some commands, such as Camltac Run or Camltac Module, accept additional attributes that change their behavior.

Locality#

The locality attributes (local, global, export) specify how Camltac modules and snippets behave when imported.

local

The Camltac module is local to the current Rocq module; it disappears when the module is closed.

global

The Camltac module is loaded when the enclosing Rocq module is Require-ed.

export

The Camltac module is loaded when the enclosing Rocq module is Import-ed.

Build directives#

Build directives are special attributes that control how the OCaml code is compiled.

libraries( package+, )

Links the given libraries before the OCaml snippet.

ppx( package+, )

Applies a list of preprocessors to the OCaml code.

Example

One can use ppx_deriving to automatically derive printers for a type:

#[ppx="ppx_deriving.show"]
Camltac Module M := ocaml:{{
  type t = A | B [@@deriving show { with_path = false }]
}}.

Camltac Eval ocaml:(return M.(show A)).- : string = "A"

compiler( compiler-flag+, )

Pass the given compilation arguments to the compiler.