diff options
Diffstat (limited to 'tactics/tacentries.mli')
| -rw-r--r-- | tactics/tacentries.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli index 70266c09f9..cb5cf8385e 100644 --- a/tactics/tacentries.mli +++ b/tactics/tacentries.mli @@ -31,6 +31,7 @@ val v_left : tactic_arg list -> tactic val v_right : tactic_arg list -> tactic val v_split : tactic_arg list -> tactic val v_clear : tactic_arg list -> tactic +val v_clear_body : tactic_arg list -> tactic val v_move : tactic_arg list -> tactic val v_move_dep : tactic_arg list -> tactic val v_apply : tactic_arg list -> tactic |