diff options
| author |  Jasper Hugunin <jasperh@cs.washington.edu> | 2018-06-04 15:47:28 -0700 |
|---|---|---|
| committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-07-01 15:42:25 -0700 |
| commit | 313e6bed17b400d638401a5c6e5d442eadb73d3a (patch) | |
| tree | 494b64ac86538e07216c5da59315168688935c6f /vernac/comInductive.mli | |
| parent | 033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff) | |
Implement uniform parameters in ComInductive
Don't allow notations attached to uniform inductives
Diffstat (limited to 'vernac/comInductive.mli')
| -rw-r--r-- | vernac/comInductive.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7ae8e8f71..4e30ed7de 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -19,9 +19,14 @@ open Decl_kinds (** Entry points for the vernacular commands Inductive and CoInductive *) +type uniform_inductive_flag = + | UniformParameters + | NonUniformParameters + val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Declarations.recursivity_kind -> unit + polymorphic -> private_flag -> uniform:uniform_inductive_flag -> + Declarations.recursivity_kind -> unit (************************************************************************) (** Internal API *) |