diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:31:30 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:31:30 +0000 |
| commit | 792a07d519a8dd396674e5431af2380a26d74b9c (patch) | |
| tree | 6454d15eee9f3c492a6ce7111692a78cfa38b95c /tactics/tactics.ml | |
| parent | 164b3bdb69f60b9bbbe83abce73c6256869d1f4b (diff) | |
Fixing buggy backtracking in "intros * pat" with failing "pat".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16549 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0595a7789..44bc4df1f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -490,11 +490,12 @@ let intros = tclREPEAT intro let intro_erasing id = tclTHEN (thin [id]) (introduction id) let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac = - let rec aux ids = - tclORELSE0 - (intro_then_gen loc name_flag move_flag false dep_flag - (fun id -> aux (id::ids))) - (tac ids) in + let rec aux ids gl = + try + intro_then_gen loc name_flag move_flag false dep_flag + (fun id -> aux (id::ids)) gl + with RefinerError IntroNeedsProduct -> + tac ids gl in aux [] let rec get_next_hyp_position id = function |