diff options
| author | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-11 16:55:29 +0200 |
| commit | 99cdbc25a3a92545544a087ed55240c488b42fc9 (patch) | |
| tree | 4b9f80d7ae15a421b5745dec138759a37cf68da6 /printing | |
| parent | 1c620d266885086e076011917d5b1d28af299ea1 (diff) | |
Fix bug #3289
Diffstat (limited to 'printing')
| -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 16759a3d83..5cad4806d4 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -728,7 +728,7 @@ let rec pr_vernac = function str":" ++ spc () ++ pr_constr cl ++ pr_priority pri ++ (match props with - | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr p + | Some (_,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) | VernacContext l -> |