diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1e3e7b48ac..6121b3a1ec 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -15,7 +15,6 @@ open Esubst (** Flags for profiling reductions. *) val stats : bool ref -val share : bool ref val with_stats: 'a Lazy.t -> 'a @@ -106,8 +105,13 @@ type 'a infos = { i_cache : 'a infos_cache } val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env -> - (existential -> constr option) -> 'a infos +val create: + repr:('a infos -> 'a infos_tab -> constr -> 'a) -> + share:bool -> + reds -> + env -> + (existential -> constr option) -> + 'a infos val create_tab : unit -> 'a infos_tab val evar_value : 'a infos_cache -> existential -> constr option |