From 8750682e367d7e78634bf88e667e4c9e7c3613d3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 10:22:25 +0200
Subject: Remove cache in Heads

This cache makes the pretyper depend on components that should morally
be higher-level (Libobject and co), so I'd like to see how critical this
cache is before taking any action.
---
 interp/declare.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 08a6ac5f7b..717f8ef49a 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -119,7 +119,6 @@ let set_declare_scheme f = declare_scheme := f
 
 let update_tables c =
   declare_constant_implicits c;
-  Heads.declare_head (EvalConstRef c);
   Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
 
 let register_side_effect (c, role) =
@@ -257,7 +256,6 @@ let declare_variable id obj =
   let oname = add_leaf id (inVariable (Inr (id,obj))) in
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
-  Heads.declare_head (EvalVarRef id);
   oname
 
 (** Declaration of inductive blocks *)
-- 
cgit v1.2.3