new intro:

[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 a4b2bde6879231b7f8ad716d1f115144f43392b0..822421a24eebe3716663c45d765712aaccaa2a07 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -11,6 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+val print_tac: bool -> string -> 's NTacStatus.tactic
+
 val dot_tac: 's NTacStatus.tactic
 val branch_tac: ?force:bool -> 's NTacStatus.tactic
 val shift_tac: 's NTacStatus.tactic
@@ -41,6 +43,8 @@ val elim_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic
 val intro_tac: string -> 's NTacStatus.tactic
+val intros_tac: 
+     ?names_ref:string list ref -> string list -> 's NTacStatus.tactic
 val cases_tac: 
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
      's NTacStatus.tactic