diff options
| author | Arnaud Spiwack | 2014-07-29 14:07:42 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-29 17:16:29 +0200 |
| commit | cf04daec997ae431b14dd3a3bbf0db22013b3c71 (patch) | |
| tree | 4c200f515b5dbb061133f38d7908157be400864d /printing | |
| parent | 9e8316d8fd6a13966c21ef77d5fcba270bc9a32a (diff) | |
Untyped terms in tactic: function [type_term c] to give a typed version of [c].
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7fc214304f..2b7f2babd1 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -940,6 +940,7 @@ and pr_tacarg = function | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c | UConstr c -> str"uconstr:" ++ pr_constr c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l + | TacPretype c -> str "fresh" ++ pr_constr c | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la |