diff options
| author | Hugo Herbelin | 2017-03-13 23:06:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-15 14:50:53 +0100 |
| commit | 671e5ad1795b2606a5da9c65758fb0d337c4d14e (patch) | |
| tree | 60de8f2d83355269cb07050d14a97b712bb959d4 /printing/miscprint.ml | |
| parent | 0e07ace6b6810f70f99fffff924d8c499db18250 (diff) | |
Attempt to improve error message when "apply in" fail.
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
Diffstat (limited to 'printing/miscprint.ml')
| -rw-r--r-- | printing/miscprint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/miscprint.ml b/printing/miscprint.ml index 7b2c5695fd..360843711c 100644 --- a/printing/miscprint.ml +++ b/printing/miscprint.ml @@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function | IntroInjection pl -> str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ str "]" - | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c | IntroRewrite true -> str "->" | IntroRewrite false -> str "<-" |