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