diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d7b269a1de..5fff21e270 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -303,7 +303,9 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * simple_binder with_coercion list - | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of + bool (*[false] => assume positive*) * + private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of |