diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index ee578669c2..e33aa38173 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -355,7 +355,7 @@ let destruct_ind sigma c = then avoid should be [| lb_An ... lb _A1 (resp. bl_An ... bl_A1) eq_An .... eq_A1 An ... A1 |] -so from Ai we can find the the correct eq_Ai bl_ai or lb_ai +so from Ai we can find the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) let do_replace_lb mode lb_scheme_key aavoid narg p q = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 9824172315..5258ab2ea4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1987,8 +1987,9 @@ let vernac_subproof gln = match gln with | None -> Proof.focus subproof_cond () 1 p | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p + | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" - (str "Brackets only support the single numbered goal selector.")) + (str "Brackets do not support multi-goal selectors.")) let vernac_end_subproof () = Proof_global.simple_with_current_proof (fun _ p -> |