From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/declareops.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'kernel/declareops.mli') diff --git a/kernel/declareops.mli b/kernel/declareops.mli index fb46112e..35490cee 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -11,7 +11,6 @@ open Declarations open Mod_subst open Univ -open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool val is_opaque : constant_body -> bool -(** Side effects *) - -val string_of_side_effect : side_effect -> string - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool @@ -66,6 +61,11 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool (** Is the inductive cumulative? *) val inductive_is_cumulative : mutual_inductive_body -> bool +val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj_arg:int -> + Names.Projection.Repr.t option +val inductive_make_projections : Names.inductive -> mutual_inductive_body -> + Names.Projection.Repr.t array option + (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) -- cgit v1.2.3