diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7b9eb68d59..6c5d9e485e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -29,6 +29,8 @@ module Stack : sig | Update of 'a and 'a t = 'a member list + val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val empty : 'a t val compare_shape : 'a t -> 'a t -> bool (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)]. @@ -77,6 +79,8 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state +val pr_state : state -> Pp.std_ppcmds + (** {6 Machinery about a stack of unfolded constant } cst applied to params must convertible to term of the state applied to args |