diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2entries.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index c26fbdc478..95a5f954c6 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -750,14 +750,14 @@ let perform_eval e = Proof_global.give_me_the_proof () with Proof_global.NoCurrentProof -> let sigma = Evd.from_env env in - Vernacexpr.SelectAll, Proof.start sigma [] + Goal_select.SelectAll, Proof.start sigma [] in let v = match selector with - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i v - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l v - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id v - | Vernacexpr.SelectAll -> v - | Vernacexpr.SelectAlreadyFocused -> assert false (** TODO **) + | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v + | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v + | Goal_select.SelectId id -> Proofview.tclFOCUSID id v + | 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 |