From 19198167d9324386dcaa6c49b032410a9eeaff55 Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 11 Apr 2006 15:12:48 +0000
Subject: adding a new tactic [intro_avoiding idl] which acts as intro but
 prevents the new identifier to bellong to [idl]

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8698 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml  | 2 ++
 tactics/tactics.mli | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18d2d5fec3..c9d249dfb2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -303,6 +303,8 @@ let intro_force force_flag = intro_gen (IntroAvoid []) None force_flag
 let intro = intro_force false
 let introf = intro_force true
 
+let intro_avoiding l = intro_gen (IntroAvoid l) None false 
+
 let introf_move_name destopt = intro_gen (IntroAvoid []) destopt true
 
 (* For backwards compatibility *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1c7967e10a..79dd4d291e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -63,6 +63,9 @@ val intro                : tactic
 val introf               : tactic
 val intro_force          : bool -> tactic
 val intro_move           : identifier option -> identifier option -> tactic
+  (* [intro_avoiding idl] acts as intro but prevents the new identifier
+     to belong to [idl] *)
+val intro_avoiding       : identifier list -> tactic
 
 val intro_replacing      : identifier -> tactic
 val intro_using          : identifier -> tactic
-- 
cgit v1.2.3