Importing the tactic in other files

One important aspect of Camltac is that Camltac modules follow Rocq’s locality system, i.e., they can be made #[local], #[export], or #[global].

Create a new file called Test.v that simply imports Tutorial.v:

Test.v

Require Import Tutorial.

By default, Camltac modules are #[export], but we can make this explicit in Tutorial.v:

Tutorial.v

#[export]
Camltac Module ApplySearch := ocaml:{{
  (* … *)

In Test.v, you can check that ApplySearch was imported using Camltac Check:

Camltac Check ApplySearch.
val create_pattern : Environ.env -> Evd.evar_map -> constr -> Ltac2.pattern
val search :
  Environ.env -> Evd.evar_map -> Ltac2.pattern -> Ltac2.reference list
val print_results : Ltac2.reference list -> unit
val run : unit -> unit tactic