diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-21 20:45:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-21 22:02:11 +0200 |
| commit | cfd8ec82784a5c893b63f3c82736eb76fe487ad7 (patch) | |
| tree | 6023b404ea2bab422eebae013b564dccd97da57f /printing | |
| parent | 3f6c0abc4d434d14d47681e4142ff7b927294f64 (diff) | |
Removing decompose record / sum from the tactic 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 587a8db41..0dabe3a26 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -718,10 +718,6 @@ and pr_atom1 = function (str "double induction" ++ pr_arg pr_quantified_hypothesis h1 ++ pr_arg pr_quantified_hypothesis h2) - | TacDecomposeAnd c -> - hov 1 (str "decompose record" ++ pr_constrarg c) - | TacDecomposeOr c -> - hov 1 (str "decompose sum" ++ pr_constrarg c) | TacDecompose (l,c) -> hov 1 (str "decompose" ++ spc () ++ hov 0 (str "[" ++ prlist_with_sep spc pr_ind l |