diff options
| author | Pierre Boutillier | 2014-04-23 10:02:51 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-05-26 15:24:31 +0200 |
| commit | 0f980482bcde723a5fdea00a511863e88f1284f9 (patch) | |
| tree | ddbdcc94045f7f9fc0420dede96435e63e5f584f /pretyping/reductionops.mli | |
| parent | 983798aff23e67007108320e6968603134a4dde3 (diff) | |
cbn: args list instead of arg number
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 } *) |