diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cbv.ml | 24 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 24 |
2 files changed, 29 insertions, 19 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 520bcd6b41..bac13a0bd7 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -241,8 +241,6 @@ module VNativeEntries = let float_ty env = VAL(0, mkConst @@ get_float_type env) - let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env) - let mkCarry env b e = let (c0,c1) = get_carry_constructors env in CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|]) @@ -270,15 +268,21 @@ module VNativeEntries = let (_eq,_lt,gt) = get_cmp_constructors env in CONSTR(Univ.in_punivs gt, [||]) - let mkSomeCmp env v = - let cmp_ty = cmp_ty env in - let (some,_none) = get_option_constructors env in - CONSTR(Univ.in_punivs some, [|cmp_ty;v|]) + let mkFLt env = + let (_eq,lt,_gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs lt, [||]) + + let mkFEq env = + let (eq,_lt,_gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs eq, [||]) + + let mkFGt env = + let (_eq,_lt,gt,_nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs gt, [||]) - let mkNoneCmp env = - let cmp_ty = cmp_ty env in - let (_some,none) = get_option_constructors env in - CONSTR(Univ.in_punivs none, [|cmp_ty|]) + let mkFNotComparable env = + let (_eq,_lt,_gt,nc) = get_f_cmp_constructors env in + CONSTR(Univ.in_punivs nc, [||]) end module VredNative = RedNative(VNativeEntries) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 12419c04bc..321c64e411 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -891,15 +891,21 @@ struct let (_eq, _lt, gt) = get_cmp_constructors env in mkConstruct gt - let mkSomeCmp env v = - let cmp_ty = mkConst @@ get_cmp_type env in - let (some, _none) = get_option_constructors env in - mkApp(mkConstruct some, [|cmp_ty;v|]) - - let mkNoneCmp env = - let cmp_ty = mkConst @@ get_cmp_type env in - let (_some, none) = get_option_constructors env in - mkApp(mkConstruct none, [|cmp_ty|]) + let mkFLt env = + let (_eq, lt, _gt, _nc) = get_f_cmp_constructors env in + mkConstruct lt + + let mkFEq env = + let (eq, _lt, _gt, _nc) = get_f_cmp_constructors env in + mkConstruct eq + + let mkFGt env = + let (_eq, _lt, gt, _nc) = get_f_cmp_constructors env in + mkConstruct gt + + let mkFNotComparable env = + let (_eq, _lt, _gt, nc) = get_f_cmp_constructors env in + mkConstruct nc end module CredNative = RedNative(CNativeEntries) |