diff options
Diffstat (limited to 'tactics/hiddentac.mli')
| -rw-r--r-- | tactics/hiddentac.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index f5b35e57d..dc547c2a8 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -80,9 +80,6 @@ val h_rename : identifier -> identifier -> tactic (* Constructors *) -(* -val h_any_constructor : tactic -> tactic -*) val h_constructor : int -> constr bindings -> tactic val h_left : constr bindings -> tactic val h_right : constr bindings -> tactic |