From 243ffa4b928486122075762da6ce8da707e07daf Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 Aug 2014 00:02:45 +0200 Subject: 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. --- tactics/tacenv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/tacenv.ml') 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 -- cgit v1.2.3