diff options
Diffstat (limited to 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 84359a36b..25d79582f 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -82,11 +82,8 @@ val alpha_rt : Id.t list -> glob_constr -> glob_constr (* same as alpha_rt but for case branches *) val alpha_br : Id.t list -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr -> - Loc.t * Id.t list * Glob_term.cases_pattern list * - Glob_term.glob_constr - + Glob_term.cases_clause -> + Glob_term.cases_clause (* Reduction function *) val replace_var_by_term : |