diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 22:13:04 +0200 |
| commit | 32716cc80cbda47e59e26c920ffb0ab738b0e9c0 (patch) | |
| tree | aa30dbcd367b5079f6308f9d9fad0c62b70bc964 /printing | |
| parent | cc3f28467f826506b8eb6e07c3b2db9ffd2ed3ba (diff) | |
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 5dbf9a42a..7949bafcb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -507,9 +507,8 @@ module Make | ipat -> spc() ++ prc c ++ pr_as_ipat prdc ipat - let pr_by_tactic prt = function - | Some tac -> keyword "by" ++ spc () ++ prt tac - | None -> mt() + let pr_by_tactic prt tac = + spc() ++ keyword "by" ++ spc () ++ prt tac let pr_hyp_location pr_id = function | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs @@ -822,7 +821,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_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + pr_by_tactic (pr.pr_tactic ltop) tac ) | TacAssert (_,None,ipat,c) -> hov 1 ( @@ -905,7 +904,7 @@ module Make ) (* Equality and inversion *) - | TacRewrite (ev,l,cl,tac) -> + | TacRewrite (ev,l,cl,by) -> hov 1 ( primitive (with_evars ev "rewrite") ++ spc () ++ prlist_with_sep @@ -915,7 +914,11 @@ 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 - ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac + ++ ( + match by with + | Some by -> pr_by_tactic (pr.pr_tactic ltop) by + | None -> mt() + ) ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( |