diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 001ae6adf5c3a926058af6a431626f4553c3f4d0 (patch) | |
| tree | 7e023a8827b37bcd6eb0c743c3791416edf60be5 | |
| parent | 080f60258407d8cf0f8991f763bafe1b6363ac57 (diff) | |
Revert "Fixing printing of Polymorphic/Monomorphic."
This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 6670aa41ab..4056115785 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -518,7 +518,7 @@ module Make match v with | VernacPolymorphic (poly, v) -> let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in - return (s ++ spc () ++ pr_vernac v) + return (s ++ pr_vernac v) | VernacProgram v -> return (keyword "Program" ++ spc() ++ pr_vernac v) | VernacLocal (local, v) -> |