diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 17:24:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-03 16:51:09 +0200 |
| commit | 64637ffc5054199459d9fc7f07b84a99da71c6f1 (patch) | |
| tree | b5b5c4774e217aa1df50f5921dfa2e445b799b62 /ltac/tacinterp.ml | |
| parent | 2c01bd7b446c1151922ad0a01c3dc6b85f5bea54 (diff) | |
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.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 10 |
1 files changed, 0 insertions, 10 deletions
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"<exact>") begin |