diff options
| author | Pierre-Marie Pédrot | 2019-05-14 23:21:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-14 23:21:34 +0200 |
| commit | 2a60906dd9d295615bcfa4b1fce8cea9626d965f (patch) | |
| tree | 5681d71e2cd4c038fcff690dfbc3f9d3f994bb87 /user-contrib | |
| parent | 75262c3f8af195a83673ff06a53d0fd0bd23b57e (diff) | |
| parent | 06b60655b98580baab98f35f6c89716e2381934c (diff) | |
Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 9fd01426de..254c2e5086 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -740,7 +740,6 @@ let register_redefinition ?(local = false) qid e = Lib.add_anonymous_leaf (inTac2Redefinition def) let perform_eval ~pstate e = - let open Proofview.Notations in let env = Global.env () in let (e, ty) = Tac2intern.intern ~strict:false e in let v = Tac2interp.interp Tac2interp.empty_environment e in @@ -761,12 +760,8 @@ let perform_eval ~pstate e = | Goal_select.SelectAll -> v | Goal_select.SelectAlreadyFocused -> assert false (* TODO **) in - (* HACK: the API doesn't allow to return a value *) - let ans = ref None in - let tac = (v >>= fun r -> ans := Some r; Proofview.tclUNIT ()) in - let (proof, _) = Proof.run_tactic (Global.env ()) tac proof in + let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let sigma = Proof.in_proof proof (fun sigma -> sigma) in - let ans = match !ans with None -> assert false | Some r -> r in let name = int_name () in Feedback.msg_notice (str "- : " ++ pr_glbtype name (snd ty) ++ spc () ++ str "=" ++ spc () ++ |