diff options
| author | Pierre-Marie Pédrot | 2016-03-05 20:08:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-05 20:09:58 +0100 |
| commit | 70e0d022333e0fc9e06b582f6831cbc698959cf0 (patch) | |
| tree | 91987abbeb9eb9ac1c26674740412550b80b19bd /printing/pptactic.ml | |
| parent | ebaa67508ec9f59f95e5b68bfece6228e2024ce5 (diff) | |
| parent | 18a5eb4ecfcb7c2fbb315719c09e3d5fc0a3574e (diff) | |
Generalizing the uses of tactic scopes everywhere.
This feature allows the user to write "let x := open_constr(foo) in ..." for instance
without having to resort to tactic notations. Some changes have been introduced in
the parsing of ad-hoc argument scopes, e.g. one has to put parentheses around
constr:(...) and ltac:(...) in tactics. This breaks badly written scripts, although
it is easy to be forward-compatible by preemptively putting thoses parentheses.
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 36863906ea..fdc1288aec 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -696,7 +696,6 @@ module Make type 'a printer = { pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; pr_constr : 'trm -> std_ppcmds; - pr_uconstr : 'utrm -> std_ppcmds; pr_lconstr : 'trm -> std_ppcmds; pr_dconstr : 'dtrm -> std_ppcmds; pr_pattern : 'pat -> std_ppcmds; @@ -711,7 +710,6 @@ module Make constraint 'a = < term :'trm; - utrm :'utrm; dterm :'dtrm; pattern :'pat; constant :'cst; @@ -1153,8 +1151,6 @@ module Make pr.pr_reference r | ConstrMayEval c -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c - | UConstr c -> - keyword "uconstr:" ++ pr.pr_uconstr c | TacFreshId l -> keyword "fresh" ++ pr_fresh_ids l | TacPretype c -> @@ -1182,7 +1178,6 @@ module Make let pr = { pr_tactic = pr_raw_tactic_level; pr_constr = pr_constr_expr; - pr_uconstr = pr_constr_expr; pr_dconstr = pr_constr_expr; pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; @@ -1213,7 +1208,6 @@ module Make let pr = { pr_tactic = prtac; pr_constr = pr_and_constr_expr (pr_glob_constr_env env); - pr_uconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env); pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env); @@ -1255,7 +1249,6 @@ module Make let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; - pr_uconstr = pr_closed_glob_env env Evd.empty; pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); pr_lconstr = pr_lconstr_env env Evd.empty; pr_pattern = pr_constr_pattern_env env Evd.empty; |