diff options
| author | Hugo Herbelin | 2014-09-11 14:53:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-11 15:11:58 +0200 |
| commit | 7ec643712e5376bc2a3f71d4673947b94c60415f (patch) | |
| tree | 71264003c5b5a42f23f1253b31a0508bb5f1b291 | |
| parent | 5ab7efb4d32b05b3ab967d46bc59a0bc853bbae2 (diff) | |
Keeping a sub-optimal behavior of intros_possibly_replacing for compatibility with inversion
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca1e25fbe8..90a89458eb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -656,12 +656,15 @@ let intro_replacing id gl = (* This version assumes that replacement is actually possible *) (* (ids given in the introduction order) *) +(* We keep a sub-optimality in cleaing for compatibility with *) +(* the behavior of inversion *) let intros_possibly_replacing ids = + let suboptimal = true in Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let posl = List.map (fun id -> (id,get_next_hyp_position id hyps)) ids in Tacticals.New.tclTHEN - (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) (List.rev ids)) + (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) (if suboptimal then ids else List.rev ids)) (Tacticals.New.tclMAP (fun (id,pos) -> Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id)) posl) |