From 968b70d36371f7335e677a6f13578d1e317a54d9 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 5 Aug 2001 18:45:25 +0000
Subject: Elimination des coupures quand les 'clause' se réduisent à des
 hypothèses, nouveau combinateur onHyps
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1872 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacticals.mli | 25 ++++++++++++++++---------
 1 file changed, 16 insertions(+), 9 deletions(-)

(limited to 'tactics/tacticals.mli')

diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index aeaae6b4e..9bc572c6a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -64,27 +64,34 @@ i*)
 val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
-val allHyps    : goal sigma -> clause list
-val afterHyp   : identifier -> goal sigma -> clause list
-val lastHyp    : goal sigma -> clause  list
-val nLastHyps  : int -> goal sigma -> clause list
+val allHyps    : goal sigma -> identifier list
+val afterHyp   : identifier -> goal sigma -> identifier list
+val lastHyp    : goal sigma -> identifier
+val nLastHyps  : int -> goal sigma -> identifier list
+
 val allClauses : goal sigma -> clause list
 
 val onCL           : (goal sigma -> clause list) -> 
                      (clause list -> tactic) -> tactic
-val tryAllHyps     : (clause -> tactic) -> tactic
 val tryAllClauses  : (clause -> tactic) -> tactic
 val onAllClauses   : (clause -> tactic) -> tactic
 val onClause       : (clause -> tactic) -> clause -> tactic
 val onAllClausesLR : (clause -> tactic) -> tactic
-val onLastHyp      : (clause -> tactic) -> tactic
 val onNthLastHyp   : int -> (clause -> tactic) -> tactic
-val onNLastHyps    : int -> (clause -> tactic) -> tactic
 val clauseTacThen  : (clause -> tactic) -> tactic -> clause -> tactic
 val if_tac         : (goal sigma -> bool) -> tactic -> (tactic) -> tactic
 val ifOnClause     : 
-  (clause * constr -> bool) -> (clause -> tactic) -> (clause -> tactic) -> 
-    clause -> tactic
+  (clause * types -> bool) ->
+    (clause -> tactic) -> (clause -> tactic) -> clause -> tactic
+val ifOnHyp        : 
+  (identifier * types -> bool) ->
+    (identifier -> tactic) -> (identifier -> tactic) -> identifier -> tactic
+
+val onHyps         : (goal sigma -> identifier list) -> 
+                     (identifier list -> tactic) -> tactic
+val tryAllHyps     : (identifier -> tactic) -> tactic
+val onNLastHyps    : int -> (identifier -> tactic) -> tactic
+val onLastHyp      : (identifier -> tactic) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
-- 
cgit v1.2.3