diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:11:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 10:52:19 +0100 |
| commit | 1de1d505dfd1c5a05a4910cfc872971087de26fb (patch) | |
| tree | e276f4cbf43d9bc2a95ace51b86111852b1f53c4 /kernel/term_typing.mli | |
| parent | c3e26fca1d077a2b69926df85d05e067882c40b0 (diff) | |
Let definitions do not create new universe constraints.
We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.
Diffstat (limited to 'kernel/term_typing.mli')
| -rw-r--r-- | kernel/term_typing.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 4b893b056..7bc029010 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -19,7 +19,7 @@ type _ trust = | SideEffects : structure_body -> side_effects trust val translate_local_def : env -> Id.t -> section_def_entry -> - constant_def * types * Univ.ContextSet.t + constr * types val translate_local_assum : env -> types -> types @@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> Constant.t option -> +val infer_declaration : trust:'a trust -> env -> 'a constant_entry -> Cooking.result val build_constant_declaration : |