diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 84a5719374..8cbc28d1ec 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -80,10 +80,10 @@ val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic (* Constructors *) -val h_constructor : int -> open_constr bindings -> tactic -val h_left : open_constr bindings -> tactic -val h_right : open_constr bindings -> tactic -val h_split : open_constr bindings -> tactic +val h_constructor : evars_flag -> int -> open_constr bindings -> tactic +val h_left : evars_flag -> open_constr bindings -> tactic +val h_right : evars_flag -> open_constr bindings -> tactic +val h_split : evars_flag -> open_constr bindings -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic |