diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-22 14:10:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-22 14:24:58 +0200 |
| commit | 180a39219f6987b63e7cc34500371d5ce03188c4 (patch) | |
| tree | 939830a3c58e4ec3c1c641af11bf0b645a285796 /printing/pptactic.ml | |
| parent | 4d6a5677f0f4af0193bb42f5d2938287efaaf91b (diff) | |
Moving the "specialize" tactic out of the AST. Also removed an obsolete
variant of it, accepting an additional integer.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c7aff5086..6c2c67c35 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -722,10 +722,6 @@ and pr_atom1 = function hov 1 (str "decompose" ++ spc () ++ hov 0 (str "[" ++ prlist_with_sep spc pr_ind l ++ str "]" ++ pr_constrarg c)) - | TacSpecialize (n,c) -> - hov 1 (str "specialize" ++ spc () ++ pr_opt int n ++ - pr_with_bindings c) - (* Automation tactics *) | TacTrivial (_,[],Some []) as x -> pr_atom0 x | TacTrivial (d,lems,db) -> |