diff options
| author | Arnaud Spiwack | 2015-06-26 21:15:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 10:40:10 +0200 |
| commit | e0547f9e9134a9fff122df900942a094c53535c3 (patch) | |
| tree | 9b5a11a7fb28857dd26f472d6329e14a1529393a /intf | |
| parent | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (diff) | |
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 5fff21e270..ba9ac16b60 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -307,8 +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 *) locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of + bool * (* [false] => assume guarded *) locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list |