aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/uState.ml3
-rw-r--r--engine/univMinim.ml3
-rw-r--r--engine/univSubst.ml6
-rw-r--r--kernel/cooking.ml3
-rw-r--r--kernel/inductive.ml5
-rw-r--r--kernel/reduction.ml41
-rw-r--r--kernel/typeops.ml6
-rw-r--r--kernel/uGraph.ml25
-rw-r--r--kernel/vars.ml8
-rw-r--r--lib/cProfile.ml6
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/retyping.ml11
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/unification.ml6
-rw-r--r--tactics/auto.ml6
-rw-r--r--tactics/eauto.ml3
-rw-r--r--tactics/tactics.ml6
22 files changed, 10 insertions, 164 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 20ea24dd87..81559778f2 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -296,9 +296,6 @@ let add_constraints uctx cstrs =
universes = UGraph.merge_constraints cstrs' uctx.universes;
weak_constraints = weak; }
-(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
-
let add_universe_constraints uctx cstrs =
let univs, local = uctx.local in
let vars, weak, local' = process_universe_constraints uctx cstrs in
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index 4ed6e97526..86bf2c9298 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -406,6 +406,3 @@ let normalize_context_set ~lbound g ctx us algs weak =
in
let us = normalize_opt_subst us in
(us, algs), (ctx', Constraint.union noneqs eqs)
-
-(* 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 *)
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 330ed5d0ad..c76a4cd751 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -83,12 +83,6 @@ let subst_univs_constr subst c =
let f = Univ.make_subst subst in
subst_univs_fn_constr f c
-let subst_univs_constr =
- if Flags.profile then
- 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 normalize_univ_variable ~find =
let rec aux cur =
let b = find cur in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f82b754c59..87b1a71c9d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -252,9 +252,6 @@ let cook_constant { from = cb; info } =
cook_context = Some const_hyps;
}
-(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
-(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
-
(********************************)
(* Discharging mutual inductive *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index eb18d4b90e..6cb61174d3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
else
()
-(*
-let cfkey = CProfile.declare_profile "check_fix";;
-let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
-*)
-
(************************************************************************)
(* Co-fixpoints. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1e39756d47..18c3a3ec9c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -964,7 +964,8 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
compare_instances = infer_convert_instances;
compare_cumul_instances = infer_inductive_instances; }
-let gen_conv cv_pb l2r reds env evars univs t1 t2 =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _ -> None)) t1 t2 =
+ let univs = Environ.universes env in
let b =
if cv_pb = CUMUL then leq_constr_univs univs t1 t2
else eq_constr_univs univs t1 t2
@@ -974,16 +975,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
()
-(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
- let univs = Environ.universes env in
- if Flags.profile then
- 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
-
let conv_leq = gen_conv CUMUL
let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
@@ -992,7 +984,7 @@ let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
in s
-let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env t1 t2 =
let univs = Environ.universes env in
let b, cstrs =
if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
@@ -1001,37 +993,16 @@ let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
if b then cstrs
else
let state = ((univs, Univ.Constraint.empty), inferred_universes) in
- let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
+ let ((_,cstrs), _) = clos_gen_conv ts cv_pb l2r evars env univs state t1 t2 in
cstrs
-(* Profiling *)
-let infer_conv_universes =
- if Flags.profile then
- let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
- CProfile.profile7 infer_conv_universes_key infer_conv_universes
- else infer_conv_universes
-
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env t1 t2 =
- infer_conv_universes CONV l2r evars ts env t1 t2
-
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
- env t1 t2 =
- infer_conv_universes CUMUL l2r evars ts env t1 t2
+let infer_conv = infer_conv_universes CONV
+let infer_conv_leq = infer_conv_universes CUMUL
let default_conv cv_pb ?l2r:_ env t1 t2 =
gen_conv cv_pb env t1 t2
let default_conv_leq = default_conv CUMUL
-(*
-let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
-let conv_leq env t1 t2 =
- CProfile.profile4 convleqkey conv_leq env t1 t2;;
-
-let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
-let 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 1b1aa84e6b..3a946fc03a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -644,12 +644,6 @@ let infer env constr =
let constr, t = execute env constr in
make_judge constr t
-let infer =
- if Flags.profile then
- 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} =
infer_assumption env c t
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index b988ec40a7..6db54a3bb6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -251,28 +251,3 @@ type node = G.node =
let repr g = G.repr g.graph
let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
-
-(** Profiling *)
-
-let merge_constraints =
- if Flags.profile then
- 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 = 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 = 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 = 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 b09577d4db..b9991391c2 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -123,11 +123,6 @@ let substn_many lamv n c =
| _ -> Constr.map_with_binders succ substrec depth c in
substrec 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
| [] -> [||]
| hd :: tl ->
@@ -343,9 +338,6 @@ let univ_instantiate_constr u c =
assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
subst_instance_constr u c.univ_abstracted_value
-(* 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
else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
diff --git a/lib/cProfile.ml b/lib/cProfile.ml
index b68d35d2d4..7245b35d59 100644
--- a/lib/cProfile.ml
+++ b/lib/cProfile.ml
@@ -8,6 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+let enable_profile = false
+
let word_length = Sys.word_size / 8
let float_of_time t = float_of_int t /. 100.
@@ -87,9 +89,9 @@ let init_alloc = ref 0.0
let reset_profile () = List.iter reset_record !prof_table
let init_profile () =
- (* We test Flags.profile as a way to support declaring profiled
+ (* We test enable_profile as a way to support declaring profiled
functions in plugins *)
- if !prof_table <> [] || Flags.profile then begin
+ if !prof_table <> [] || enable_profile then begin
let outside = create_record () in
stack := [outside];
last_alloc := get_alloc ();
diff --git a/lib/flags.ml b/lib/flags.ml
index 57e879add7..c87a375356 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -51,8 +51,6 @@ let xml_debug = ref false
let in_debugger = ref false
let in_toplevel = ref false
-let profile = false
-
let raw_print = ref false
let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index e10e2c8cb8..2f59a0cc18 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -44,8 +44,6 @@ val xml_debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
-val profile : bool
-
(* development flag to detect race conditions, it should go away. *)
val we_are_parsing : bool ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c7bda43465..1640bff43b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -373,11 +373,6 @@ end) = struct
end
-(* let my_type_of env evars c = Typing.e_type_of env evars c *)
-(* 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 =
let evars, c = app_poly_nocheck env evd f args in
let evd', t = Typing.type_of env (goalevars evars) c in
@@ -2066,9 +2061,6 @@ let get_hyp gl (c,l) clause l2r =
let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
-(* 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 =
Proofview.Goal.enter begin fun gl ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 285fea183b..5eb8a88698 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1182,13 +1182,6 @@ let evar_conv_x flags = evar_conv_x flags
let evar_unify = conv_fun evar_conv_x
-(* Profiling *)
-let evar_conv_x =
- if Flags.profile then
- 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 ()
let evar_conv_x flags = Hook.get evar_conv_hook_get flags
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 4083d3bc23..cb576a379a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1038,13 +1038,6 @@ let nf_all env sigma =
(********************************************************************)
(* Conversion *)
(********************************************************************)
-(*
-let fkey = CProfile.declare_profile "fhnf";;
-let fhnf info v = CProfile.profile2 fkey fhnf info v;;
-
-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 =
match Conv_oracle.get_strategy (Environ.oracle e) k with
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 064990f6bf..cdb86afa1a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -249,17 +249,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
| Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
| _ -> assert false
-(* Profiling *)
-(* let get_type_of polyprop lax env sigma c = *)
-(* let f,_,_,_ = retype ~polyprop sigma in *)
-(* if lax then f env c else anomaly_on_error (f env) c *)
-
-(* 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 *)
-
let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
let f,_,_ = retype ~polyprop sigma in
if lax then f env c else anomaly_on_error (f env) c
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4e89018656..b59d4b5655 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1015,12 +1015,6 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
in app_stack (redrec (c, empty_stack))
*)
-let whd_simpl_stack =
- if Flags.profile then
- 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
reducible fix, but does this reduction of constants only until it
immediately hides a non reducible fix or a cofix *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 51b228a640..dd1d27e4c5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -242,10 +242,6 @@ let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
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 = CProfile.declare_profile "solve_typeclasses" *)
-(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
-
let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
if not (has_typeclasses filter evd) then evd
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 18db75eed5..43d562f77d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -2069,11 +2069,5 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
let w_unify env evd cv_pb flags ty1 ty2 =
w_unify env evd cv_pb ~flags:flags ty1 ty2
-let w_unify =
- if Flags.profile then
- 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 =
w_unify env evd cv_pb flags ty1 ty2
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 353e138599..0189e3ab04 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -500,12 +500,6 @@ let delta_auto debug mod_delta n lems dbnames =
(search d n mod_delta db_list hints)
end
-let delta_auto =
- if Flags.profile then
- 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
let new_auto ?(debug=Off) n = delta_auto debug true n
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 20c557b282..5df9fab236 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -359,9 +359,6 @@ let e_search_auto debug (in_depth,p) lems db_list =
tclIDTAC gl
end
-(* 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 =
Hints.wrap_hint_warning (e_search_auto debug np lems db_list)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index decf19588f..c24520b371 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1886,12 +1886,6 @@ let cut_and_apply c =
(* Exact tactics *)
(********************************************************************)
-(* let convert_leqkey = CProfile.declare_profile "convert_leq";; *)
-(* let convert_leq = CProfile.profile3 convert_leqkey convert_leq *)
-
-(* 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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:20:34 +0000