diff options
| author | jforest | 2006-07-20 15:40:36 +0000 |
|---|---|---|
| committer | jforest | 2006-07-20 15:40:36 +0000 |
| commit | 66b674a1d41d9349f4c64543eda5ef005617e3a0 (patch) | |
| tree | 2f3dd80a7270e77d8cd2e205285f1e36f9b23c70 /tactics | |
| parent | a094f618ff229f46b4efe2c00260e4e89686f173 (diff) | |
Correction du bug #1116
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9057 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
2 files changed, 9 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6196c4ecef..7664998224 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -278,6 +278,14 @@ let find_name decl gl = function if id' <> id then error ((string_of_id id)^" is already used"); id' +let find_intro_names ctxt gl = + List.rev + (List.fold_right + (fun decl idl -> find_name decl gl (IntroAvoid idl)::idl) + ctxt + []) + + let build_intro_tac id = function | None -> introduction id | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f5355eba13..9411a772bf 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -58,6 +58,7 @@ val cofix : identifier option -> tactic (*s Introduction tactics. *) val fresh_id : identifier list -> identifier -> goal sigma -> identifier +val find_intro_names : rel_context -> goal sigma -> identifier list val intro : tactic val introf : tactic |