diff options
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 082ed7ed0d..5914c4a954 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -55,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -65,9 +65,6 @@ val export_side_effects : structure_body -> env -> side_effects constant_entry -> exported_side_effect list * unit constant_entry -val constant_entry_of_side_effect : - constant_body -> seff_env -> unit constant_entry - val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body |