diff options
| author | Pierre-Marie Pédrot | 2016-06-05 21:50:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-06-15 20:21:37 +0200 |
| commit | dcf4d3e28813e09fc71f974b79ddf42d2e525976 (patch) | |
| tree | 76a95699918b818e3f6111b594b5b6ec7bd566b2 /intf | |
| parent | 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 (diff) | |
Remove the syntax changes introduced by this branch.
We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 2f2f973761..d7b269a1de 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -303,14 +303,10 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * simple_binder with_coercion list - | VernacInductive of - bool (*[false] => assume positive*) * - private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - Declarations.typing_flags * locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - Declarations.typing_flags * locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list |