diff options
| author | Pierre-Marie Pédrot | 2014-09-01 16:54:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-01 17:03:31 +0200 |
| commit | 1d6eac66b4f21a768e98d01416e4ecef68ada377 (patch) | |
| tree | 5d90b0187bf12ec89ca3d74988b450c0984e7458 /printing | |
| parent | a4d454beaafd030a5564a395d380748cf90e1b75 (diff) | |
Moving the decompose tactic out of the AST.
Diffstat (limited to 'printing')
| -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 a3a023ce9d..f3bec78e20 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -759,10 +759,6 @@ and pr_atom1 = function (str "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ pr_arg pr_quantified_hypothesis h2) - | TacDecompose (l,c) -> - hov 1 (str "decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc pr_ind l - ++ str "]" ++ pr_constrarg c)) (* Automation tactics *) | TacTrivial (_,[],Some []) as x -> pr_atom0 x | TacTrivial (d,lems,db) -> |