diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 15:34:46 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 15:34:46 +0200 |
| commit | f93b5d45ed95816cb23ce2646437bb5037a17f72 (patch) | |
| tree | e38ecd02addffe86cf05996c651fdd55034b7aaa /kernel/reduction.mli | |
| parent | 8cb3a606f7c72c32298fe028c9f98e44ea0d378b (diff) | |
| parent | d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2c1c0ec05..0bb855c67 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -10,8 +10,6 @@ open Term open Context open Environ -val left2right : bool ref - (*********************************************************************** s Reduction functions *) @@ -49,14 +47,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints -val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit - -(* val sort_cmp : *) -(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) +val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> + 'a * 'a universe_compare -> 'a * 'a universe_compare -(* val conv_sort : sorts conversion_function *) -(* val conv_sort_leq : sorts conversion_function *) +val checked_universes : UGraph.t universe_compare +val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -77,22 +72,20 @@ val conv_leq : val conv_leq_vecti : ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +(** These conversion functions are used by module subtyping, which needs to infer + universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function -val generic_conv : conv_pb -> bool -> (existential->constr option) -> +val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_nat_conv : - (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit -val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function |