diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-19 17:57:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-25 12:11:10 +0200 |
| commit | 19a7a5789c42a143f92232ce15298c2f44db96ba (patch) | |
| tree | 84f883a8a1834f7b031100822f64f6aaa15afee1 /tactics/tactics.ml | |
| parent | 965be8e6c441214542947b75e1625bc9068c40c9 (diff) | |
Fixing a bug introduced in the extension of 'apply in' + simplifying code.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 83e282a30..407f367ed 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1164,13 +1164,8 @@ let descend_in_conjunctions tac exit c = match make_projection env sigma params cstr sign elim i n c u with | None -> Tacticals.New.tclFAIL 0 (mt()) | Some (p,pt) -> - Tacticals.New.tclTHENS - (assert_before Anonymous pt) - [Proofview.V82.tactic (refine p); (* Might be ill-typed due to forbidden elimination. *) - Tacticals.New.onLastHypId (fun id -> - Tacticals.New.tclTHEN - (tac (not isrec) (mkVar id)) - (Proofview.V82.tactic (thin [id])))] + (* Might be ill-typed due to forbidden elimination. *) + tac (not isrec) p end)) | None -> raise Exit @@ -1344,7 +1339,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming Tacticals.New.tclTHEN (apply_clear_request clear_flag false c) (tac id)) - with e when with_destruct -> + with e when with_destruct && when Errors.noncritical e -> let e = Errors.push e in descend_in_conjunctions aux (fun _ -> raise e) c end |