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 /tactics | |
| parent | 3bd97f637e6d24e9cb5b409adf8b54e8e55d2f14 (diff) | |
Allow run_tactic to return a value, remove hack from ltac2
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 4aa4d13e1e..6efa1ece9c 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -204,10 +204,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature."); *) let pf = Proof.start ~name ~poly (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in - let pf = - fst (Proof.run_tactic env ( - tclTHEN intro (onLastHypId inv_op)) pf) - in + let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in let global_named_context = Global.named_context_val () in let ownSign = ref begin |