diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 17:27:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 18:03:50 +0100 |
| commit | 0b644da20c714b01565f88dffcfd51ea8f08314a (patch) | |
| tree | 5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /printing/ppvernac.ml | |
| parent | 4953a129858a231e64dec636a3bc15a54a0e771c (diff) | |
| parent | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index ccf470946..ffec926a8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -918,8 +918,9 @@ module Make hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ keyword "Instance" ++ - (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | - Anonymous -> mt ()) ++ + (match instid with + | (loc, Name id), l -> spc () ++ pr_plident ((loc, id),l) ++ spc () + | (_, Anonymous), _ -> mt ()) ++ pr_and_type_binders_arg sup ++ str":" ++ spc () ++ pr_constr cl ++ pr_priority pri ++ |