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 c03c67c092..0224a97685 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -76,7 +76,7 @@ type red_expr = (constr, evaluable_global_reference) red_expr_gen val reduction_of_redexp : red_expr -> reduction_function -type generic_reduction_function = constr list -> reduction_function +type generic_reduction_function = constr -> reduction_function val declare_red_expr : string -> generic_reduction_function -> unit |