From b8949a0d69b5d7b2cf8759e5c4580ae0bb6a73fa Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 24 Nov 2000 00:36:05 +0000
Subject: Nouveau choix pour l'intros initial

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@938 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'tactics/tactics.mli')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b41c07ec37..ada02fcf22 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -77,6 +77,7 @@ val dyn_intros_using : tactic_arg list -> tactic
 i*)
 
 val intros_until         : identifier -> tactic
+val intros_until_n_wored : int -> tactic
 val dyn_intros_until     : tactic_arg list -> tactic
 
 val intros_clearing      : bool list -> tactic
-- 
cgit v1.2.3