diff options
Diffstat (limited to 'engine/univSubst.ml')
| -rw-r--r-- | engine/univSubst.ml | 6 |
1 files changed, 0 insertions, 6 deletions
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 |