diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 23:59:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 16:55:46 +0200 |
| commit | 52c3917be7239f7d5ab1ba882275b4571463f585 (patch) | |
| tree | 9458b71b44b5b04f649a054ace210b8382934dd3 /ltac/tacinterp.ml | |
| parent | 1654b3989041b25e3b642ffde12125344342a54b (diff) | |
Making Proof_global terminator generic in external tactics.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 177867abd..9e502682b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1969,7 +1969,6 @@ let interp_tac_gen lfun avoid_ids debug t = end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t -let _ = Proof_global.set_interp_tac interp (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) |