From c11bd7b181d6e53910dc8d39c5360f35c7b24674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 31 Aug 2017 17:28:46 +0200 Subject: Cooking.cook_constant: remove unused env argument. Unused since d95306323 (remove template polymorphic definitions). --- kernel/term_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bad449731..30127d166 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -554,7 +554,7 @@ let translate_recipe env kn r = be useless. It is detected by the dirpath of the constant being empty. *) let (_, dir, _) = Constant.repr3 kn in let hcons = DirPath.is_empty dir in - build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) + build_constant_declaration kn env (Cooking.cook_constant ~hcons r) let translate_local_def env id centry = let open Cooking in -- cgit v1.2.3