diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
| -rw-r--r-- | kernel/reduction.ml | 16 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 16 | ||||
| -rw-r--r-- | kernel/vars.ml | 12 | ||||
| -rw-r--r-- | kernel/vconv.ml | 2 |
9 files changed, 31 insertions, 31 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2579ac0456..7b921d35be 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -250,7 +250,7 @@ let cook_constant ~hcons env { from = cb; info } = cook_context = Some const_hyps; } -(* let cook_constant_key = Profile.declare_profile "cook_constant" *) -(* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) +(* let cook_constant_key = CProfile.declare_profile "cook_constant" *) +(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *) let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 62aa9a2d7b..2a629f00a9 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index a62a079da9..9f9102f7d2 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -154,7 +154,7 @@ let warn_no_native_compiler = (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin + if not Coq_config.native_compiler then begin warn_no_native_compiler (); vm_conv cv_pb env t1 t2 end diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b0f4a1e5f1..c07ac973b8 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -833,8 +833,8 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 = let gen_conv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) = let evars, univs = evars in if Flags.profile then - let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in - Profile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs + let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in + CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs else gen_conv cv_pb l2r reds env evars univs let conv = gen_conv CONV @@ -860,8 +860,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = (* Profiling *) let infer_conv_universes = if Flags.profile then - let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in - Profile.profile8 infer_conv_universes_key infer_conv_universes + let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in + CProfile.profile8 infer_conv_universes_key infer_conv_universes else infer_conv_universes let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state) @@ -895,13 +895,13 @@ let default_conv cv_pb ?(l2r=false) env t1 t2 = let default_conv_leq = default_conv CUMUL (* -let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";; +let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";; let conv_leq env t1 t2 = - Profile.profile4 convleqkey conv_leq env t1 t2;; + CProfile.profile4 convleqkey conv_leq env t1 t2;; -let convkey = Profile.declare_profile "Kernel_reduction.conv";; +let convkey = CProfile.declare_profile "Kernel_reduction.conv";; let conv env t1 t2 = - Profile.profile4 convleqkey conv env t1 t2;; + CProfile.profile4 convleqkey conv env t1 t2;; *) (* Application with on-the-fly reduction *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0e41bfc3c4..5150ad4113 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -858,7 +858,7 @@ let export ?except senv dir = } in let ast, symbols = - if !Flags.native_compiler then + if !Flags.output_native_objects then Nativelibrary.dump_library mp dir senv.env str else [], Nativecode.empty_symbols in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4ccef5c381..4a935f581a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -435,8 +435,8 @@ let infer env constr = let infer = if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) + let infer_key = CProfile.declare_profile "Fast_infer" in + CProfile.profile2 infer_key (fun b c -> infer b c) else (fun b c -> infer b c) let assumption_of_judgment env {uj_val=c; uj_type=t} = diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 00c0ea70d7..f1e8d10317 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -890,24 +890,24 @@ let dump_universes output g = let merge_constraints = if Flags.profile then - let key = Profile.declare_profile "merge_constraints" in - Profile.profile2 key merge_constraints + let key = CProfile.declare_profile "merge_constraints" in + CProfile.profile2 key merge_constraints else merge_constraints let check_constraints = if Flags.profile then - let key = Profile.declare_profile "check_constraints" in - Profile.profile2 key check_constraints + let key = CProfile.declare_profile "check_constraints" in + CProfile.profile2 key check_constraints else check_constraints let check_eq = if Flags.profile then - let check_eq_key = Profile.declare_profile "check_eq" in - Profile.profile3 check_eq_key check_eq + let check_eq_key = CProfile.declare_profile "check_eq" in + CProfile.profile3 check_eq_key check_eq else check_eq let check_leq = if Flags.profile then - let check_leq_key = Profile.declare_profile "check_leq" in - Profile.profile3 check_leq_key check_leq + let check_leq_key = CProfile.declare_profile "check_leq" in + CProfile.profile3 check_leq_key check_leq else check_leq diff --git a/kernel/vars.ml b/kernel/vars.ml index f52d734eff..eae917b5a2 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -133,8 +133,8 @@ let substn_many lamv n c = substrec n c (* -let substkey = Profile.declare_profile "substn_many";; -let substn_many lamv n c = Profile.profile3 substkey substn_many lamv n c;; +let substkey = CProfile.declare_profile "substn_many";; +let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;; *) let make_subst = function @@ -274,8 +274,8 @@ let subst_univs_constr subst c = let subst_univs_constr = if Flags.profile then - let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in - Profile.profile2 subst_univs_constr_key subst_univs_constr + let subst_univs_constr_key = CProfile.declare_profile "subst_univs_constr" in + CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr let subst_univs_level_constr subst c = @@ -347,8 +347,8 @@ let subst_instance_constr subst c = in aux c -(* let substkey = Profile.declare_profile "subst_instance_constr";; *) -(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *) +(* let substkey = CProfile.declare_profile "subst_instance_constr";; *) +(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *) let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 578a893718..3ef297b1f4 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -204,4 +204,4 @@ let vm_conv cv_pb env t1 t2 = let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () -let _ = Reduction.set_vm_conv vm_conv +let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv |