diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-31 12:53:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-31 15:09:49 +0200 |
| commit | 20c2176e8b0b64737fad8dbc1fbc9ef2d182372d (patch) | |
| tree | 6bbcc249dd6115ccd32a3e788c548cc5cdb6e1dd /tactics/tacintern.mli | |
| parent | 29bb2f7d9fecf06e3246142e649db4db0320da41 (diff) | |
Getting rid of atomic tactics in Tacenv.
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
Diffstat (limited to 'tactics/tacintern.mli')
| -rw-r--r-- | tactics/tacintern.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 84e5782f8..2f6eb60f4 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -64,6 +64,5 @@ val dump_glob_red_expr : raw_red_expr -> unit (* Hooks *) 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 |