diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6e52546f4a..ee2250b346 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -324,7 +324,7 @@ val split : constr bindings -> tactic val left_with_ebindings : evars_flag -> open_constr bindings -> tactic val right_with_ebindings : evars_flag -> open_constr bindings -> tactic -val split_with_ebindings : evars_flag -> open_constr bindings -> tactic +val split_with_ebindings : evars_flag -> open_constr bindings list -> tactic val simplest_left : tactic val simplest_right : tactic |