diff options
Diffstat (limited to 'tactics/inv.mli')
| -rw-r--r-- | tactics/inv.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/inv.mli b/tactics/inv.mli index 52804f134..d985bb7aa 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,6 +6,7 @@ open Names open Tacmach (*i*) +val half_inv_tac : identifier -> tactic val inv_tac : identifier -> tactic val inv_clear_tac : identifier -> tactic val half_dinv_tac : identifier -> tactic @@ -14,4 +15,5 @@ val dinv_clear_tac : identifier -> tactic val half_dinv_with : identifier -> Coqast.t -> tactic val dinv_with : identifier -> Coqast.t -> tactic val dinv_clear_with : identifier -> Coqast.t -> tactic + val invIn_tac : string -> identifier -> identifier list -> tactic |