summaryrefslogtreecommitdiff
path: root/kernel/cClosure.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cClosure.mli')
-rw-r--r--kernel/cClosure.mli17
1 files changed, 9 insertions, 8 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index e2f5a3b8..6121b3a1 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
@@ -152,7 +156,7 @@ type fterm =
type stack_member =
| Zapp of fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * Constant.t
+ | Zproj of Projection.Repr.t
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -239,14 +243,11 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array
val mk_clos : fconstr subs -> constr -> fconstr
val mk_clos_vect : fconstr subs -> constr array -> fconstr array
-val mk_clos_deep :
- (fconstr subs -> constr -> fconstr) ->
- fconstr subs -> constr -> fconstr
val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
-val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val to_constr : lift -> fconstr -> constr
(** End of cbn debug section i*)