diff options
| author | Hugo Herbelin | 2016-04-12 22:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:45 +0200 |
| commit | bde36d4b00185065628324d8ca71994f84eae244 (patch) | |
| tree | c4d7bba0352ee72fa31712e02882c7066a6e1ba1 /printing/pptactic.ml | |
| parent | c4d1e3113f77af2e5474fe5676c272050dd445e5 (diff) | |
In the short term, stronger invariant on the syntax of TacAssert, what
allows for a simpler re-printing of assert.
Also fixing the precedence for printing "by" clause.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7949bafcbb..5dbf9a42a3 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -507,8 +507,9 @@ module Make | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat - let pr_by_tactic prt tac = - spc() ++ keyword "by" ++ spc () ++ prt tac + let pr_by_tactic prt = function + | Some tac -> keyword "by" ++ spc () ++ prt tac + | None -> mt() let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs @@ -821,7 +822,7 @@ module Make hov 1 ( primitive (if b then "assert" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ - pr_by_tactic (pr.pr_tactic ltop) tac + pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) | TacAssert (_,None,ipat,c) -> hov 1 ( @@ -904,7 +905,7 @@ module Make ) (* Equality and inversion *) - | TacRewrite (ev,l,cl,by) -> + | TacRewrite (ev,l,cl,tac) -> hov 1 ( primitive (with_evars ev "rewrite") ++ spc () ++ prlist_with_sep @@ -914,11 +915,7 @@ module Make pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c) l ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl - ++ ( - match by with - | Some by -> pr_by_tactic (pr.pr_tactic ltop) by - | None -> mt() - ) + ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( |