diff options
Diffstat (limited to 'tactics/tacticals.ml')
-rw-r--r-- | tactics/tacticals.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 90b7d6581..074c8b9de 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -171,23 +171,23 @@ let fix_empty_or_and_pattern nv l = | IntroOrPattern [[]] -> IntroOrPattern (List.make nv []) | _ -> l -let check_or_and_pattern_size check_and loc names branchsigns = +let check_or_and_pattern_size ?loc check_and names branchsigns = let n = Array.length branchsigns in let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in let err1 p1 p2 = - user_err ~loc (str "Expects " ++ msg p1 p2 ++ str ".") in + user_err ?loc (str "Expects " ++ msg p1 p2 ++ str ".") in let errn n = - user_err ~loc (str "Expects a disjunctive pattern with " ++ int n + user_err ?loc (str "Expects a disjunctive pattern with " ++ int n ++ str " branches.") in let err1' p1 p2 = - user_err ~loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in - let errforthcoming loc = - user_err ~loc (strbrk "Unexpected non atomic pattern.") in + user_err ?loc (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in + let errforthcoming ?loc = + user_err ?loc (strbrk "Unexpected non atomic pattern.") in match names with | IntroAndPattern l -> if not (Int.equal n 1) then errn n; let l' = List.filter (function _,IntroForthcoming _ -> true | _,IntroNaming _ | _,IntroAction _ -> false) l in - if l' != [] then errforthcoming (fst (List.hd l')); + if l' != [] then errforthcoming ~loc:(fst (List.hd l')); if check_and then let p1 = List.count (fun x -> x) branchsigns.(0) in let p2 = List.length branchsigns.(0) in @@ -195,7 +195,7 @@ let check_or_and_pattern_size check_and loc names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (Loc.ghost,IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (Loc.tag @@ IntroNaming IntroAnonymous) l) else names else @@ -208,20 +208,20 @@ let check_or_and_pattern_size check_and loc names branchsigns = err1' p1 p2 else errn n; names -let get_and_check_or_and_pattern_gen check_and loc names branchsigns = - let names = check_or_and_pattern_size check_and loc names branchsigns in +let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns = + let names = check_or_and_pattern_size ?loc check_and names branchsigns in match names with | IntroAndPattern l -> [|l|] | IntroOrPattern l -> Array.of_list l -let get_and_check_or_and_pattern = get_and_check_or_and_pattern_gen true +let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true let compute_induction_names_gen check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] | Some (loc,names) -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in - get_and_check_or_and_pattern_gen check_and loc names branchletsigns + get_and_check_or_and_pattern_gen check_and ~loc names branchletsigns let compute_induction_names = compute_induction_names_gen true |