diff options
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 420ae8d74..6ea0505a0 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -63,7 +63,7 @@ val get_debug : unit -> debug_info (* Adds a definition for tactics in the table *) val add_tacdef : - bool -> (identifier Util.located * raw_tactic_expr) list -> unit + bool -> (identifier Util.located * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) |