aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2016-12-12 14:18:48 +0100
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2016-12-12 14:18:48 +0100
commit90b61424761c5ba1ddbecf20c29d78b485584ae7 (patch)
tree5143571cdc885ebae5b0754efff18114644a8be8 /kernel/kernel.mllib
parentad768e435a736ca51ac79a575967b388b34918c7 (diff)
Extend Fast_typeops to be a replacement for Typeops
This brings the fix in cad44fc for #2996 to the copy of Fast_typeops.check_hyps_inclusion. Fast_typeops.constant_type checks the universe constraints instead of outputting them. Since everyone who used Typeops.constant_type just discarded the constraints they've been switched to constant_type_in which should be the same in Fast_typeops and Typeops. There are some small differences in the interfaces: - Typeops.type_of_projection <-> Fast_typeops.type_of_projection_constant to avoid collision with the internally used type_of_projection (which gives the type of [Proj(p,c)]). - check_hyps_inclusion takes [('a -> constr)] and ['a] instead of [constr] for reporting errors.
Diffstat (limited to 'kernel/kernel.mllib')
0 files changed, 0 insertions, 0 deletions