diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 00:02:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-18 01:15:43 +0200 |
| commit | 243ffa4b928486122075762da6ce8da707e07daf (patch) | |
| tree | 3870e1b1d3059ba13158a73df7c5f3b300e504ce /tactics/tacenv.ml | |
| parent | 6dd9e003c289a79b0656e7c6f2cc59935997370c (diff) | |
Moving the TacExtend node from atomic to plain tactics.
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
Diffstat (limited to 'tactics/tacenv.ml')
| -rw-r--r-- | tactics/tacenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 62b9904d7..63aea6f43 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,7 +26,7 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) -(** ML tactic extensions (TacExtend) *) +(** ML tactic extensions (TacML) *) type ml_tactic = typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic |