From d782dabc61251834e35a77c43e070ea8b4e0b04a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 May 2019 21:59:18 +0200
Subject: Centralize the hashconsing of constant declarations.

Safe_typing is now responsible for hashconsing of all accessible structures,
except for opaque terms which are handled by Opaqueproof.
---
 kernel/term_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 592a97e132..fd0f2a18e4 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -35,7 +35,7 @@ val translate_constant :
   'a trust -> env -> Constant.t -> 'a constant_entry ->
     Opaqueproof.proofterm constant_body
 
-val translate_recipe : hcons:bool -> env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
+val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-- 
cgit v1.2.3