diff options
| author | Maxime Dénès | 2019-04-05 10:22:25 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-05 10:22:25 +0200 |
| commit | 8750682e367d7e78634bf88e667e4c9e7c3613d3 (patch) | |
| tree | 5a62ebfa1b482c37727ccca2ab18e088fb282ade /pretyping/heads.mli | |
| parent | be6f3a6234ee809dd3c290621d80c3280a41355e (diff) | |
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.
Diffstat (limited to 'pretyping/heads.mli')
| -rw-r--r-- | pretyping/heads.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/pretyping/heads.mli b/pretyping/heads.mli index 421242996c..e5f9967590 100644 --- a/pretyping/heads.mli +++ b/pretyping/heads.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names open Constr open Environ @@ -17,11 +16,6 @@ open Environ provides the function to compute the head symbols and a table to store the heads *) -(** [declared_head] computes and registers the head symbol of a - possibly evaluable constant or variable *) - -val declare_head : evaluable_global_reference -> unit - (** [is_rigid] tells if some term is known to ultimately reduce to a term with a rigid head symbol *) |