diff options
| author | Arnaud Spiwack | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /printing | |
| parent | 64e94267cb80adc1b4df782cc83a579ee521b59b (diff) | |
Assume totality: dedicated type rather than bool
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 93cd35472a..8a8521ccc1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -806,7 +806,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (chkguard,local, recs) -> + | VernacFixpoint (flags,local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -821,11 +821,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (chkguard,local, corecs) -> + | VernacCoFixpoint (flags,local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -838,7 +838,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> |