diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index dc547c2a85..847d0caa75 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -73,7 +73,7 @@ val h_lapply : constr -> tactic (* Context management *) -val h_clear : identifier list -> tactic +val h_clear : bool -> identifier list -> tactic val h_clear_body : identifier list -> tactic val h_move : bool -> identifier -> identifier -> tactic val h_rename : identifier -> identifier -> tactic |