diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 15:01:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:48 +0200 |
| commit | 90252e973f5bcafc5f3b0b18564612d7fb4503a8 (patch) | |
| tree | c74f29db0ee113a17e505a734a8e04646ecc9e10 | |
| parent | 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a (diff) | |
Temporary hack to restore missing printing of "constr:" in right-hand
side of Ltac's "let ... in ..." or "match ... with ... => ... end".
Example:
Ltac f x := let x := 0 in constr:(S x).
Print Ltac f.
has a missing "constr:".
Note: for generic arguments: "ltac:" is always used, even if a constr, etc.
| -rw-r--r-- | printing/pptactic.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 920f1d62a..f58452176 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -949,6 +949,13 @@ 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 @@ -967,9 +974,10 @@ module Make let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag (pr_ltac_constr (pr_tac ltop)) llc ++ spc () ++ keyword "in" - ) ++ fnl () ++ pr_tac (llet,E) u), + ) ++ fnl () + ++ pr_ltac_constr (pr_tac (llet,E)) u), llet | TacMatch (lz,t,lrul) -> hov 0 ( @@ -977,7 +985,7 @@ module Make ++ pr_tac ltop t ++ spc () ++ keyword "with" ++ prlist (fun r -> fnl () ++ str "| " - ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r + ++ pr_match_rule true (pr_ltac_constr (pr_tac ltop)) pr.pr_lpattern r ) lrul ++ fnl() ++ keyword "end"), lmatch @@ -987,14 +995,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_tac ltop) pr.pr_lpattern r + ++ pr_match_rule false (pr_ltac_constr (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_tac (lfun,E) body), + ++ pr_ltac_constr (pr_tac (lfun,E)) body), lfun | TacThens (t,tl) -> hov 1 ( |