diff options
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 9e5cb48a49..c43fc46239 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Esubst @@ -29,7 +29,7 @@ val all_opaque : transparent_state val all_transparent : transparent_state val is_transparent_variable : transparent_state -> variable -> bool -val is_transparent_constant : transparent_state -> constant -> bool +val is_transparent_constant : transparent_state -> Constant.t -> bool (** Sets of reduction kinds. *) module type RedFlagsSig = sig @@ -46,7 +46,7 @@ module type RedFlagsSig = sig val fFIX : red_kind val fCOFIX : red_kind val fZETA : red_kind - val fCONST : constant -> red_kind + val fCONST : Constant.t -> red_kind val fVAR : Id.t -> red_kind (** No reduction at all *) @@ -61,6 +61,9 @@ module type RedFlagsSig = sig (** Adds a reduction kind to a set *) val red_add_transparent : reds -> transparent_state -> reds + (** Retrieve the transparent state of the reduction flags *) + val red_transparent : reds -> transparent_state + (** Build a reduction set from scratch = iter [red_add] on [no_red] *) val mkflags : red_kind list -> reds @@ -92,7 +95,7 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = constant puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey type 'a infos_cache type 'a infos = { @@ -122,8 +125,8 @@ type fterm = | FAtom of constr (** Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive puniverses - | FConstruct of constructor puniverses + | FInd of inductive Univ.puniverses + | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array | FProj of projection * fconstr | FFix of fixpoint * fconstr subs @@ -145,7 +148,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * Constant.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -163,6 +166,7 @@ val stack_tail : int -> stack -> stack val stack_nth : stack -> int -> fconstr val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack +val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use |