From 10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 15:22:31 +0100 Subject: Using "l" printer for glob_constr, like for constr. This is to avoid excessive parentheses, in particular when printing "constr:()" in "Print Ltac f". --- plugins/ltac/pptactic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669..ab07e0c24 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1250,8 +1250,8 @@ let () = ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + Ppconstr.pr_lconstr_expr + (fun (c, _) -> Printer.pr_lglob_constr c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 -- cgit v1.2.3 From b9c6982fb5f60f720fd4c0435414406a9ecca749 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 16:44:27 +0100 Subject: Fixing printing of tactics encapsulated as tacarg with Tacexp. We preserve the level instead of resetting it at level 0. Probably it would be the same as giving level ltop since Tacexp apparently comes only from using a tactic in an Ltac "let", which is where I observed a problem. --- plugins/ltac/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index ab07e0c24..bc0de0acd 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1003,7 +1003,7 @@ let pr_goal_selector ~toplevel s = | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> -- cgit v1.2.3 From a83c37de529f12348cd9e3a66a38c58b72777478 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 15:24:16 +0100 Subject: Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). Was broken since 8.6. --- plugins/ltac/pptactic.ml | 29 +++++++++++++++++++++++------ test-suite/output/ltac.out | 7 +++++++ test-suite/output/ltac.v | 11 +++++++++++ 3 files changed, 41 insertions(+), 6 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index bc0de0acd..3f885f8ba 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,14 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -536,15 +544,24 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (na,(bl,t)) = + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) + str " :=" ++ brk (1,1) ++ pr t) - let pr_let_clauses recflag pr = function + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -858,7 +875,7 @@ let pr_goal_selector ~toplevel s = 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.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 35c3057d8..c5d58ec1e 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -31,3 +31,10 @@ nat nat 0 0 +Ltac foo := + let x := intros ** in + let y := intros -> in + let v := constr:(nil) in + let w := () in + let z := 1 in + pose v diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 76c37625a..6adbe95dd 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end. match goal with H: context [?x*?y] |- _ => idtac x end. match goal with |- context [?x*?y] => idtac x end. Abort. + +(* Check printing of let in Ltac and Tactic Notation *) + +Ltac foo := + let x := intros in + let y := intros -> in + let v := constr:(@ nil True) in + let w := () in + let z := 1 in + pose v. +Print Ltac foo. -- cgit v1.2.3