diff options
| author | Gaëtan Gilbert | 2019-05-09 14:07:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-14 14:14:26 +0200 |
| commit | 682ec8fe694e37757d2cd6c98fb5e2e609a6f08f (patch) | |
| tree | 2a219924d4cabdd100679d92d8512346d874ac1d /proofs/pfedit.ml | |
| parent | 3bd97f637e6d24e9cb5b409adf8b54e8e55d2f14 (diff) | |
Allow run_tactic to return a value, remove hack from ltac2
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 4f36354f79..52e15f466f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr = else tac in let env = Global.env () in - let (p,(status,info)) = Proof.run_tactic env tac pr in + let (p,(status,info),()) = Proof.run_tactic env tac pr in let env = Global.env () in let sigma = Evd.from_env env in let () = @@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = let prev_future_goals = save_future_goals sigma in (* Start a proof *) let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _) = + let (prf, _, ()) = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (* Catch the inner error of the monad tactic *) |