diff options
| author | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-02 15:04:57 +0200 |
| commit | fd146ca38202c9843b4240cbdac0ae75f57e4d67 (patch) | |
| tree | 39f0c957c4ea02e6976299b4183b6bcfa8ea9f7a /vernac | |
| parent | 48ec42bb91b8c0fb4d5930e62e29a408de594482 (diff) | |
| parent | fca82378cd2824534383f1f5bc09d08fade1dc17 (diff) | |
Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 564c0965bd..f0e41d27cc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -909,7 +909,7 @@ let vernac_set_used_variables e = if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (Pfedit.solve SelectAll None tac p), () + fst (Pfedit.solve Goal_select.SelectAll None tac p), () end (*****************************) @@ -1611,7 +1611,7 @@ let get_current_context_of_args = function let query_command_selector ?loc = function | None -> None - | Some (SelectNth n) -> Some n + | Some (Goal_select.SelectNth n) -> Some n | _ -> user_err ?loc ~hdr:"query_command_selector" (str "Query commands only support the single numbered goal selector.") @@ -1911,7 +1911,7 @@ let vernac_subproof gln = Proof_global.simple_with_current_proof (fun _ p -> match gln with | None -> Proof.focus subproof_cond () 1 p - | Some (SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets only support the single numbered goal selector.")) |