diff options
| author | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
| commit | 3bc0c82700a805e889198b810cc0148f6479cbe1 (patch) | |
| tree | eac2cce0546a79cb5786e0570c0c55b9b4438e4b /kernel/cClosure.mli | |
| parent | 7456164386a87df83763109e12fa8aaa71a96104 (diff) | |
| parent | 14a1786158ec093faa172a5b95a93b06ad43b7af (diff) | |
Merge PR #7085: Turn the kernel reduction sharing flag into an argument passed in the cache
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 |