diff options
| author | Arnaud Spiwack | 2014-07-30 12:12:21 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-01 19:18:58 +0200 |
| commit | 78692ad28ded4f94d5cf7e54240fe0b71d1be282 (patch) | |
| tree | 05ccc456677d61f2d6b34dff334641059d179193 /printing | |
| parent | 47c688165c6ad00b725bc4f93574bba55c2544f5 (diff) | |
Add [numgoal] to Ltac.
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 e812086d95..2aadde7c16 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -941,6 +941,7 @@ and pr_tacarg = function | UConstr c -> str"uconstr:" ++ pr_constr c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacPretype c -> str "type_term" ++ pr_constr c + | TacNumgoals -> str "numgoals" | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la |