diff options
Diffstat (limited to 'pretyping/tacred.mli')
| -rw-r--r-- | pretyping/tacred.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index db59787a1..6e0479fb1 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -62,7 +62,7 @@ val fold_commands : constr list -> reduction_function (** Pattern *) val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> - constr + evar_map * constr (** Rem: Lazy strategies are defined in Reduction *) |