diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:43:34 +0100 |
commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
tree | aefad2e3de35f75c46729f9310d33b56d3821961 /kernel/declareops.mli | |
parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'kernel/declareops.mli')
-rw-r--r-- | kernel/declareops.mli | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af97..1b870095 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool |