diff options
| author | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:02 +0200 |
| commit | 3011cbfb224b3b2dfb72afd05094614b97a2128b (patch) | |
| tree | 4bf6607f8a29238bac0d87775d74f2105a1b9384 | |
| parent | 4b9cf206fec3ef9be52fdef67d564e3edc21eb5a (diff) | |
Revert "Temporary hack to restore missing printing of "constr:" in right-hand"
This reverts commit 90252e973f5bcafc5f3b0b18564612d7fb4503a8.
| -rw-r--r-- | printing/pptactic.ml | 18 |
1 files changed, 5 insertions, 13 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f584521765..920f1d62a0 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -949,13 +949,6 @@ module Make let make_pr_tac pr strip_prod_binders tag_atom tag = - let pr_ltac_constr pr = function - | TacArg (_,TacGeneric arg) - | TacArg (_,Tacexp (TacArg (_,TacGeneric arg))) as u - when argument_type_eq (genarg_tag arg) (ArgumentType wit_constr) - -> keyword "constr:" ++ surround (pr u) - | u -> pr u in - let extract_binders = function | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body) | body -> ([],body) in @@ -974,10 +967,9 @@ module Make let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_ltac_constr (pr_tac ltop)) llc + pr_let_clauses recflag (pr_tac ltop) llc ++ spc () ++ keyword "in" - ) ++ fnl () - ++ pr_ltac_constr (pr_tac (llet,E)) u), + ) ++ fnl () ++ pr_tac (llet,E) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -985,7 +977,7 @@ module Make ++ pr_tac ltop t ++ spc () ++ keyword "with" ++ prlist (fun r -> fnl () ++ str "| " - ++ pr_match_rule true (pr_ltac_constr (pr_tac ltop)) pr.pr_lpattern r + ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r ) lrul ++ fnl() ++ keyword "end"), lmatch @@ -995,14 +987,14 @@ module Make ++ keyword (if lr then "match reverse goal with" else "match goal with") ++ prlist (fun r -> fnl () ++ str "| " - ++ pr_match_rule false (pr_ltac_constr (pr_tac ltop)) pr.pr_lpattern r + ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r ) lrul ++ fnl() ++ keyword "end"), lmatch | TacFun (lvar,body) -> hov 2 ( keyword "fun" ++ prlist pr_funvar lvar ++ str " =>" ++ spc () - ++ pr_ltac_constr (pr_tac (lfun,E)) body), + ++ pr_tac (lfun,E) body), lfun | TacThens (t,tl) -> hov 1 ( |