aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/vernacexpr.mli')
-rw-r--r--intf/vernacexpr.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ba9ac16b6..2f2f97376 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