From 8c6092e8c43a74a8a175a532580284124c06e34f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Oct 2017 23:50:11 +0200 Subject: Adding support for syntax "let _ := e in e'" in Ltac. Adding a file fixing #5996 and which uses this feature. --- plugins/ltac/pptactic.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/ltac/pptactic.ml') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e467d3e2c..28a13fb40 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -536,8 +536,8 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (id,(bl,t)) = - hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ + let pr_let_clause k pr (na,(bl,t)) = + hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) let pr_let_clauses recflag pr = function -- cgit v1.2.3