aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-14 19:24:14 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-19 17:46:51 +0100
commit06931bf4b193f978d43f30e22732b0122602ed53 (patch)
treeef3a5748aca905ba6417a04f80134307c7fd47b9
parentef09beee5057251ce066e05be2fa118abc8d09e9 (diff)
record: restore API declare_projections (removed in e414c07e1)
-rw-r--r--vernac/record.mli11
1 files changed, 11 insertions, 0 deletions
diff --git a/vernac/record.mli b/vernac/record.mli
index e632e7bbf..e0a4b8fdd 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -13,6 +13,17 @@ open Globnames
val primitive_flag : bool ref
+val declare_projections :
+ inductive ->
+ Entries.constant_universes_entry ->
+ ?kind:Decl_kinds.definition_object_kind ->
+ Id.t ->
+ bool list ->
+ Universes.universe_binders ->
+ Impargs.manual_implicits list ->
+ Context.Rel.t ->
+ (Name.t * bool) list * Constant.t option list
+
val definition_structure :
inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list *