diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 7 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 11 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 6 |
6 files changed, 0 insertions, 41 deletions
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 |