From 64637ffc5054199459d9fc7f07b84a99da71c6f1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 17:24:05 +0100 Subject: Removing "intro" from the tactic AST. Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead. --- ltac/tacinterp.ml | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'ltac/tacinterp.ml') diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index f6f988ee2..c8fa9367f 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1644,16 +1644,6 @@ and interp_atomic ist tac : unit Proofview.tactic = expected behaviour. *) (Tactics.intro_patterns l')) sigma end } - | TacIntroMove (ido,hto) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let mloc = interp_move_location ist env sigma hto in - let ido = Option.map (interp_ident ist env sigma) ido in - name_atomic ~env - (TacIntroMove(ido,mloc)) - (Tactics.intro_move ido mloc) - end } | TacExact c -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin -- cgit v1.2.3