instance fixed

[helm.git] / helm / software / components / ng_tactics / nTactics.mli

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index ab049f1c34fdc3495536a45c97f0273580c84e2b..b8659c3574fe63dfb34a170f052e2649408bc70f 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -15,12 +15,14 @@ val dot_tac: 's NTacStatus.tactic
 val branch_tac: 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
 val pos_tac: int list -> 's NTacStatus.tactic
+val case_tac: string -> 's NTacStatus.tactic
 val wildcard_tac: 's NTacStatus.tactic
 val merge_tac: 's NTacStatus.tactic
 val focus_tac: int list -> 's NTacStatus.tactic
 val unfocus_tac: 's NTacStatus.tactic
 val skip_tac: 's NTacStatus.tactic
 val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
+val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
 
 val distribute_tac:
  NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
@@ -31,6 +33,7 @@ val assumption_tac: 's NTacStatus.tactic
 val change_tac: 
    where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term -> 
      's NTacStatus.tactic
+val cut_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
 val elim_tac: 
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
@@ -39,6 +42,7 @@ val cases_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
 val case1_tac: string -> 's NTacStatus.tactic
+val lapply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
 val rewrite_tac:
   dir:[ `LeftToRight | `RightToLeft ] ->
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
@@ -55,6 +59,5 @@ val assert_tac:
  ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
   's NTacStatus.tactic
 
-val auto_tac:
-  params:(NTacStatus.tactic_term list * (string * string) list) -> 
-   's NTacStatus.tactic
+val constructor_tac : 
+        ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic