diff options
| -rw-r--r-- | checker/inductive.ml | 4 | ||||
| -rw-r--r-- | dev/doc/debugging.md | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 4 | ||||
| -rw-r--r-- | engine/universes.ml | 4 | ||||
| -rw-r--r-- | kernel/cooking.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/reduction.ml | 16 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 16 | ||||
| -rw-r--r-- | kernel/vars.ml | 12 | ||||
| -rw-r--r-- | lib/cProfile.ml (renamed from lib/profile.ml) | 0 | ||||
| -rw-r--r-- | lib/cProfile.mli (renamed from lib/profile.mli) | 0 | ||||
| -rw-r--r-- | lib/lib.mllib | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 4 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 8 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 4 | ||||
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/eauto.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 |
25 files changed, 67 insertions, 67 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 1271a02b0..22353ec16 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1070,8 +1070,8 @@ let check_fix env ((nvect,_),(names,_,bodies as _recdef) as fix) = done (* -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/dev/doc/debugging.md b/dev/doc/debugging.md index 7d3d811cc..fa145d498 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -73,8 +73,8 @@ Per function profiling To profile function foo in file bar.ml, add the following lines, just after the definition of the function: - let fookey = Profile.declare_profile "foo";; - let foo a b c = Profile.profile3 fookey foo a b c;; + let fookey = CProfile.declare_profile "foo";; + let foo a b c = CProfile.profile3 fookey foo a b c;; where foo is assumed to have three arguments (adapt using Profile.profile1, Profile. profile2, etc). diff --git a/engine/uState.ml b/engine/uState.ml index c28e78f7d..9510371be 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -236,8 +236,8 @@ let add_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } -(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) -(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) +(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *) +(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *) let add_universe_constraints ctx cstrs = let univs, local = ctx.uctx_local in diff --git a/engine/universes.ml b/engine/universes.ml index 0250295fd..30490ec56 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -946,8 +946,8 @@ let normalize_context_set ctx us algs = let us = normalize_opt_subst us in (us, algs), (ctx', Constraint.union noneqs eqs) -(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) -(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) +(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *) let is_trivial_leq (l,d,r) = Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 2579ac045..7b921d35b 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 62aa9a2d7..2a629f00a 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/reduction.ml b/kernel/reduction.ml index 41d6c05eb..ca67c5f13 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/typeops.ml b/kernel/typeops.ml index 4ccef5c38..4a935f581 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 00c0ea70d..f1e8d1031 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 f52d734ef..eae917b5a 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/lib/profile.ml b/lib/cProfile.ml index 0bc226a45..0bc226a45 100644 --- a/lib/profile.ml +++ b/lib/cProfile.ml diff --git a/lib/profile.mli b/lib/cProfile.mli index cae4397a1..cae4397a1 100644 --- a/lib/profile.mli +++ b/lib/cProfile.mli diff --git a/lib/lib.mllib b/lib/lib.mllib index 8791f0741..66f939a91 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -9,7 +9,7 @@ System CThread Spawn Trie -Profile +CProfile Explore Predicate Rtree diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7..ee34161dd 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -2084,8 +2084,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e5776d2ec..cb8844623 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2f8e5b964..30fc5f321 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1269,11 +1269,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index f8f086fad..00b175c48 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 85383ba39..5a522e06a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 2e213a51d..b49da57a4 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 84ffab426..08329391d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 3e3313eb5..cd2b10906 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -30,8 +30,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) diff --git a/tactics/auto.ml b/tactics/auto.ml index fa8435d1f..e7e21b5f4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -514,8 +514,8 @@ let delta_auto debug mod_delta n lems dbnames = let delta_auto = if Flags.profile then - let key = Profile.declare_profile "delta_auto" in - Profile.profile5 key delta_auto + let key = CProfile.declare_profile "delta_auto" in + CProfile.profile5 key delta_auto else delta_auto let auto ?(debug=Off) n = delta_auto debug false n diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f5c6ab879..b5cfbe68b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -405,8 +405,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl = pr_info_nop d; user_err Pp.(str "eauto: search failed") -(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *) -(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *) +(* let e_search_auto_key = CProfile.declare_profile "e_search_auto" *) +(* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = tclTRY (e_search_auto debug np lems db_list) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e072bd95f..cb2a77558 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1976,11 +1976,11 @@ let cut_and_apply c = (* Exact tactics *) (********************************************************************) -(* let convert_leqkey = Profile.declare_profile "convert_leq";; *) -(* let convert_leq = Profile.profile3 convert_leqkey convert_leq *) +(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *) +(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *) -(* let refine_no_checkkey = Profile.declare_profile "refine_no_check";; *) -(* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *) +(* let refine_no_checkkey = CProfile.declare_profile "refine_no_check";; *) +(* let refine_no_check = CProfile.profile2 refine_no_checkkey refine_no_check *) let exact_no_check c = Refine.refine ~typecheck:false (fun h -> (h,c)) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 553da2dc0..b62396317 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -756,7 +756,7 @@ let init_toplevel arglist = (* Coq's init process, phase 1: - OCaml parameters, and basic structures and IO *) - Profile.init_profile (); + CProfile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in @@ -846,7 +846,7 @@ let start () = let sigma, env = Pfedit.get_current_context () in Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; - Profile.print_profile (); + CProfile.print_profile (); exit 0 (* [Coqtop.start] will be called by the code produced by coqmktop *) |