diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-22 23:50:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-04 14:12:45 +0100 |
| commit | 8c6092e8c43a74a8a175a532580284124c06e34f (patch) | |
| tree | ece4db520837006b2e3bffcc165b7c76a45b1bd1 /plugins/ltac/pptactic.ml | |
| parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) | |
Adding support for syntax "let _ := e in e'" in Ltac.
Adding a file fixing #5996 and which uses this feature.
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 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 |