diff options
| author | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-31 16:58:29 +0200 |
| commit | eed90d1bd867dce59f6bf1b2bf769fff188f128b (patch) | |
| tree | cfbf3bb666b23d0ddce9ea3c370c54eb4a87a150 /plugins/ltac/pptactic.ml | |
| parent | 23588ea0ccacd7e0071cbbad3328d871414f37c6 (diff) | |
| parent | bbde815f8108f4641f5411d03f7a88096cc2221b (diff) | |
Merge PR#248: Adding eassert, eset, epose, etc.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a001c6a2ba..4e254ea766 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -768,15 +768,15 @@ type 'a extra_genarg_printer = primitive "cofix" ++ spc () ++ pr_id id ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l ) - | TacAssert (b,Some tac,ipat,c) -> + | TacAssert (ev,b,Some tac,ipat,c) -> hov 1 ( - primitive (if b then "assert" else "enough") ++ + primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" 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 ) - | TacAssert (_,None,ipat,c) -> + | TacAssert (ev,_,None,ipat,c) -> hov 1 ( - primitive "pose proof" + primitive (if ev then "epose proof" else "pose proof") ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ) | TacGeneralize l -> @@ -786,11 +786,11 @@ type 'a extra_genarg_printer = pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) - | TacLetTac (na,c,cl,b,e) -> + | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (ev,na,c,cl,b,e) -> hov 1 ( - (if b then primitive "set" else primitive "remember") ++ + primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c else pr_pose_as_style pr.pr_constr na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ |