diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-01 22:08:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-01 22:08:39 +0000 |
| commit | 6e78a98aaa51df2975595a6adcbe263febbccadc (patch) | |
| tree | c37ceecbc5fc2438f60a64e5e31b3eb87a780f6a /tactics/tacticals.mli | |
| parent | 22656ee48b22b4b34024cd4bf262d0de279540f9 (diff) | |
Ajout tactiques Rename et Pose; modifications pour Inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index bb3aa3761..a984d791f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -65,9 +65,9 @@ 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 -> identifier list -val afterHyp : identifier -> goal sigma -> identifier list +val afterHyp : identifier -> goal sigma -> named_context val lastHyp : goal sigma -> identifier -val nLastHyps : int -> goal sigma -> identifier list +val nLastHyps : int -> goal sigma -> named_context val allClauses : goal sigma -> clause list @@ -87,10 +87,10 @@ val ifOnHyp : (identifier * types -> bool) -> (identifier -> tactic) -> (identifier -> tactic) -> identifier -> tactic -val onHyps : (goal sigma -> identifier list) -> - (identifier list -> tactic) -> tactic +val onHyps : (goal sigma -> named_context) -> + (named_context -> tactic) -> tactic val tryAllHyps : (identifier -> tactic) -> tactic -val onNLastHyps : int -> (identifier -> tactic) -> tactic +val onNLastHyps : int -> (named_declaration -> tactic) -> tactic val onLastHyp : (identifier -> tactic) -> tactic (* [ConclPattern concl pat tacast]: @@ -113,7 +113,7 @@ type branch_args = { type branch_assumptions = { ba : branch_args; (* the branch args *) - assums : identifier list; (* the list of assumptions introduced *) + assums : named_context; (* the list of assumptions introduced *) cargs : identifier list; (* the constructor arguments *) constargs : identifier list; (* the CONSTANT constructor arguments *) recargs : identifier list; (* the RECURSIVE constructor arguments *) |