diff options
| author | Maxime Dénès | 2017-11-13 11:11:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 11:11:44 +0100 |
| commit | 1f9dcdee40d95ee56ef91876579f2c059939e04a (patch) | |
| tree | a018b8cddb19e2f909238e74311f59f1ab284003 /plugins/ltac/pptactic.ml | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
| parent | 8c6092e8c43a74a8a175a532580284124c06e34f (diff) | |
Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e467d3e2ca..28a13fb404 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 |