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 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ba9ac16b60..2f2f973761 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -307,10 +307,10 @@ type vernac_expr = bool (*[false] => assume positive*) * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - bool * (* [false] => assume guarded *) + Declarations.typing_flags * locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - bool * (* [false] => assume guarded *) + Declarations.typing_flags * locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list |