diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index bbf95c7056..f4486bf0c8 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -116,6 +116,12 @@ let wrap f = let wrap_unit f = return () >>= fun () -> f (); return v_unit +let assert_focussed = + Proofview.Goal.goals >>= fun gls -> + match gls with + | [_] -> Proofview.tclUNIT () + | [] | _ :: _ :: _ -> throw err_notfocussed + let pf_apply f = Proofview.Goal.goals >>= function | [] -> @@ -682,6 +688,7 @@ end (** unit -> constr *) let () = define0 "goal" begin + assert_focussed >>= fun () -> Proofview.Goal.enter_one begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in return (Value.of_constr concl) |