diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-12 22:25:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | e2d4490b12514362af8e1f0b8b89cf0550f78130 (patch) | |
| tree | ddb275621606524ccd6af7b5a9b94b36988041c0 /printing | |
| parent | 613d99b98d3c78213a69acdbf23c660764487300 (diff) | |
A 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')
| -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 5356cdee8..3779a9412 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -567,8 +567,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 @@ -871,7 +872,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 ( @@ -937,7 +938,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 @@ -947,11 +948,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 ( |