[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

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