diff options
| author | Jim Fehrle | 2018-11-16 14:33:12 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2018-11-16 14:42:17 -0800 |
| commit | 9780a52ccf75a4d837b640536d8023aaeb2fb18a (patch) | |
| tree | d7628489a003853600658068d4a8141fead25506 /plugins/ssr/ssrequality.ml | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
Remove SSR profiling
Deletes the SsrProfiling and SsrMatchingProfiling options
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2a69e3f23a..22475fef34 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -425,11 +425,6 @@ let rwcltac cl rdx dir sr gl = in tclTHEN cvtac' rwtac gl -let prof_rwcltac = mk_profiler "rwrxtac.rwcltac";; -let rwcltac cl rdx dir sr gl = - prof_rwcltac.profile (rwcltac cl rdx dir sr) gl -;; - [@@@ocaml.warning "-3"] let lz_coq_prod = @@ -455,8 +450,6 @@ let ssr_is_setoid env = Rewrite.is_applied_rewrite_relation env sigma [] (EConstr.mkApp (r, args)) <> None -let prof_rwxrtac_find_rule = mk_profiler "rwrxtac.find_rule";; - let closed0_check cl p gl = if closed0 cl then errorstrm Pp.(str"No occurrence of redex "++ pr_constr_env (pf_env gl) (project gl) p) @@ -556,7 +549,6 @@ let rwrxtac occ rdx_pat dir rule gl = d, (ise, Evd.evar_universe_context ise, Reductionops.nf_evar ise r) with _ -> rwtac rs in rwtac rules in - let find_rule rdx = prof_rwxrtac_find_rule.profile find_rule rdx in let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in let find_R, conclude = match rdx_pat with | Some (_, (In_T _ | In_X_In_T _)) | None -> @@ -582,11 +574,6 @@ let rwrxtac occ rdx_pat dir rule gl = rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl ;; -let prof_rwxrtac = mk_profiler "rwrxtac";; -let rwrxtac occ rdx_pat dir rule gl = - prof_rwxrtac.profile (rwrxtac occ rdx_pat dir rule) gl -;; - let ssrinstancesofrule ist dir arg gl = let sigma0, env0, concl0 = project gl, pf_env gl, pf_concl gl in let rule = interp_term ist gl arg in |