diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-11-22 19:34:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-11-23 15:28:41 +0100 |
| commit | ff0a051caf031fb427007714f6325c74b8893702 (patch) | |
| tree | fbb4b2fae772c9a0fe6a8b5d7310eb60dae7c045 /toplevel/record.mli | |
| parent | c81065e5cdc6d803bd67eccf93dc8fbb640c6892 (diff) | |
Pass around information on the use of template polymorphism for
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
Diffstat (limited to 'toplevel/record.mli')
| -rw-r--r-- | toplevel/record.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/record.mli b/toplevel/record.mli index 2422b45bd..cead9b6f6 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -29,6 +29,7 @@ val declare_structure : Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> Univ.universe_context -> Id.t -> Id.t -> manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *) + bool (** template arity ? *) -> Impargs.manual_explicitation list list -> rel_context -> (** fields *) ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t -> bool -> (** coercion? *) |