diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 18873d1c6..238a329fd 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -67,7 +67,8 @@ val get_debug : unit -> debug_info (* Adds a definition for tactics in the table *) val add_tacdef : - bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit + Vernacexpr.locality_flag -> bool -> + (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) |