diff options
| author | herbelin | 2011-04-08 14:08:41 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-08 14:08:41 +0000 |
| commit | 49fced31608d06ab672982c0a46d22b75e6f00f1 (patch) | |
| tree | 4547d6f3807782ac3652e05e996f21497a6bf732 /kernel/type_errors.ml | |
| parent | 92a5f74259977cc3f92d8b822bdb727a95e64bc6 (diff) | |
Fixing multiple printing bugs with "Notation f x := ..."
- Missing space and bad constr level in "About f"
- Display of arguments missing when used as a pattern notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13966 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions