diff options
| author | Enrico Tassi | 2018-04-05 10:04:07 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-05 10:04:07 +0200 |
| commit | 4c3564ac7e2ea231a6dde84f2af6bfddbc0834c6 (patch) | |
| tree | ba0f9bbbc04048c48a2128dde5bb89b2517e52c8 /printing | |
| parent | f97498a6c104da9b7b31f84505db76194a566f9b (diff) | |
| parent | bca95952b541b209a3f8ca44d1ff119b976e54fb (diff) | |
Merge PR #7016: Make parsing independent of the cumulativity flag.
Diffstat (limited to 'printing')
| -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 bbf0e2b605..7eb8396ac8 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -767,8 +767,9 @@ open Decl_kinds if p then let cm = match cum with - | GlobalCumulativity | LocalCumulativity -> "Cumulative" - | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + | Some VernacCumulative -> "Cumulative" + | Some VernacNonCumulative -> "NonCumulative" + | None -> "" in cm ^ " " ^ kind else kind |