diff options
| author | Hugo Herbelin | 2014-08-02 09:30:30 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:21 +0200 |
| commit | 0e6facc70506d81e765c5a0be241a77bc7b22b85 (patch) | |
| tree | ba0f92d3bf019d5cbf4c72b2f2b667457052f179 /printing | |
| parent | f9517286637fd0891a3ac1aac041b437e157f756 (diff) | |
Adding a syntax "enough" for the variant of "assert" with the order of
subgoals and the role of the "by tac" clause swapped.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 0039a81bfe..dbf83936af 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -682,11 +682,11 @@ and pr_atom1 = function | TacMutualCofix (id,l) -> hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++ str"with " ++ prlist_with_sep spc pr_cofix_tac l) - | TacAssert (Some tac,ipat,c) -> - hov 1 (str "assert" ++ + | TacAssert (b,Some tac,ipat,c) -> + hov 1 (str (if b then "assert" else "enough") ++ pr_assumption pr_lconstr pr_constr ipat c ++ pr_by_tactic (pr_tac_level ltop) tac) - | TacAssert (None,ipat,c) -> + | TacAssert (_,None,ipat,c) -> hov 1 (str "pose proof" ++ pr_assertion pr_lconstr pr_constr ipat c) | TacGeneralize l -> |