diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 466f3a4d17..b4eaf27d50 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -111,6 +111,8 @@ module Cst_stack : sig val add_args : constr array -> t -> t val add_cst : constr -> t -> t val best_cst : t -> (constr * constr list) option + val best_state : state -> t -> state + val pr : t -> Pp.std_ppcmds end (** {6 Reduction Function Operators } *) |