diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 14:58:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 15:39:10 +0200 |
| commit | b52dca14d3ac66ecd1657a21fecd0b48751096a7 (patch) | |
| tree | 193b1f22f433b24dd8038e54c2e96041acc6dd19 /tactics/tacintern.mli | |
| parent | 0736cd1ff1eb07c6faae43cdfbe2efd11c8470e9 (diff) | |
Qualified ML tactic names. The plugin name is used to discriminate
potentially conflicting tactics names from different plugins.
Diffstat (limited to 'tactics/tacintern.mli')
| -rw-r--r-- | tactics/tacintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 22588fcf1..84e5782f8 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -63,7 +63,7 @@ val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr val dump_glob_red_expr : raw_red_expr -> unit (* Hooks *) -val assert_tactic_installed_hook : (string -> unit) Hook.t +val assert_tactic_installed_hook : (ml_tactic_name -> unit) Hook.t val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t val strict_check : bool ref |