[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

6 files changed, 65 insertions, 67 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 63f923dfd3..768d6860dc 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -31,7 +31,7 @@ let absurd c =
     let env = Proofview.Goal.env gl in
     let sigma = Sigma.to_evar_map sigma in
     let j = Retyping.get_judgment_of env sigma c in
-    let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
+    let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
     let tac =
     Tacticals.New.tclTHENLIST [
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ae7446c82..ace7c30e90 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1462,7 +1462,7 @@ let simpleInjClause with_evars = function
   | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
 
 let injConcl = injClause None false None
-let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
+let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
 
 let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter { enter = begin fun gl ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 904a17417a..f2147db40a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -283,7 +283,7 @@ let generalizeRewriteIntros as_mode tac depids id =
   end }
 
 let error_too_many_names pats =
-  let loc = Loc.join_loc (fst (List.hd pats)) (fst (List.last pats)) in
+  let loc = Loc.merge (fst (List.hd pats)) (fst (List.last pats)) in
   Proofview.tclENV >>= fun env ->
   tclZEROMSG ~loc (
     str "Unexpected " ++
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 90b7d6581a..074c8b9de8 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
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3b90ec514a..d60196213e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -116,7 +116,7 @@ type branch_assumptions = private {
    error message if |pats| <> |branchsign|; extends them if no pattern is given
    for let-ins in the case of a conjunctive pattern *)
 val get_and_check_or_and_pattern :
-  Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
+  ?loc:Loc.t -> delayed_open_constr or_and_intro_pattern_expr ->
   bool list array -> intro_patterns array
 
 (** Tolerate "[]" to mean a disjunctive pattern of any length *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e792585822..7dad90242c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -53,8 +53,6 @@ module NamedDecl = Context.Named.Declaration
 
 let inj_with_occurrences e = (AllOccurrences,e)
 
-let dloc = Loc.ghost
-
 let typ_of env sigma c =
   let open Retyping in
   try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c
@@ -427,11 +425,11 @@ let default_id env sigma decl =
 type name_flag =
   | NamingAvoid of Id.t list
   | NamingBasedOn of Id.t * Id.t list
-  | NamingMustBe of Loc.t * Id.t
+  | NamingMustBe of Id.t Loc.located
 
 let naming_of_name = function
   | Anonymous -> NamingAvoid []
-  | Name id -> NamingMustBe (dloc,id)
+  | Name id -> NamingMustBe (Loc.tag id)
 
 let find_name mayrepl decl naming gl = match naming with
   | NamingAvoid idl ->
@@ -469,7 +467,7 @@ let assert_before_gen b naming t =
   assert_before_then_gen b naming t (fun _ -> Proofview.tclUNIT ())
 
 let assert_before na = assert_before_gen false (naming_of_name na)
-let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
+let assert_before_replacing id = assert_before_gen true (NamingMustBe (Loc.tag id))
 
 let assert_after_then_gen b naming t tac =
   let open Context.Rel.Declaration in
@@ -488,7 +486,7 @@ let assert_after_gen b naming t =
   assert_after_then_gen b naming t (fun _ -> (Proofview.tclUNIT ()))
 
 let assert_after na = assert_after_gen false (naming_of_name na)
-let assert_after_replacing id = assert_after_gen true (NamingMustBe (dloc,id))
+let assert_after_replacing id = assert_after_gen true (NamingMustBe (Loc.tag id))
 
 (**************************************************************)
 (*          Fixpoints and CoFixpoints                         *)
@@ -969,7 +967,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   end }
 
 let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
-let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false
+let intro_mustbe_force id = intro_gen (NamingMustBe (Loc.tag id)) MoveLast true false
 let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
 
 let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
@@ -979,7 +977,7 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
 let intro_move_avoid idopt avoid hto = match idopt with
   | None -> intro_gen (NamingAvoid avoid) hto true false
-  | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
+  | Some id -> intro_gen (NamingMustBe (Loc.tag id)) hto true false
 
 let intro_move idopt hto = intro_move_avoid idopt [] hto
 
@@ -1139,7 +1137,7 @@ let try_intros_until tac = function
 let rec intros_move = function
   | [] -> Proofview.tclUNIT ()
   | (hyp,destopt) :: rest ->
-      Tacticals.New.tclTHEN (intro_gen (NamingMustBe (dloc,hyp)) destopt false false)
+      Tacticals.New.tclTHEN (intro_gen (NamingMustBe (Loc.tag hyp)) destopt false false)
 	(intros_move rest)
 
 let run_delayed env sigma c =
@@ -1291,7 +1289,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
     error_uninstantiated_metas new_hyp_typ clenv;
   let new_hyp_prf = clenv_value clenv in
   let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
-  let naming = NamingMustBe (dloc,targetid) in
+  let naming = NamingMustBe (Loc.tag targetid) in
   let with_clear = do_replace (Some id) naming in
   Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd))
@@ -1798,13 +1796,13 @@ let apply_with_delayed_bindings_gen b e l =
         (one k f) (aux cbl)
   in aux l
 
-let apply_with_bindings cb = apply_with_bindings_gen false false [None,(dloc,cb)]
+let apply_with_bindings cb = apply_with_bindings_gen false false [None,(Loc.tag cb)]
 
-let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(dloc,cb)]
+let eapply_with_bindings cb = apply_with_bindings_gen false true [None,(Loc.tag cb)]
 
-let apply c = apply_with_bindings_gen false false [None,(dloc,(c,NoBindings))]
+let apply c = apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))]
 
-let eapply c = apply_with_bindings_gen false true [None,(dloc,(c,NoBindings))]
+let eapply c = apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))]
 
 let apply_list = function
   | c::l -> apply_with_bindings (c,ImplicitBindings l)
@@ -2216,7 +2214,7 @@ let constructor_tac with_evars expctdnumopt i lbind =
 	(Proofview.Goal.env gl) sigma (fst mind, i) in
       let cons = mkConstructU (cons, EInstance.make u) in
 	
-      let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in
+      let apply_tac = general_apply true false with_evars None (Loc.tag (cons,lbind)) in
       let tac =
 	(Tacticals.New.tclTHENLIST
            [
@@ -2301,7 +2299,7 @@ let my_find_eq_data_decompose gl t =
       -> None
   | Constr_matching.PatternMatchingFailure -> None
 
-let intro_decomp_eq loc l thin tac id =
+let intro_decomp_eq ?loc l thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2309,13 +2307,13 @@ let intro_decomp_eq loc l thin tac id =
   match my_find_eq_data_decompose gl t with
   | Some (eq,u,eq_args) ->
     !intro_decomp_eq_function
-    (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l)
+    (fun n -> tac ((Loc.tag id)::thin) (Some (true,n)) l)
     (eq,t,eq_args) (c, t)
   | None ->
     Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end }
 
-let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
+let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
   Proofview.Goal.enter { enter = begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
@@ -2323,7 +2321,7 @@ let intro_or_and_pattern loc with_evars bracketed ll thin tac id =
   let branchsigns = compute_constructor_signatures false ind in
   let nv_with_let = Array.map List.length branchsigns in
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
-  let ll = get_and_check_or_and_pattern loc ll branchsigns in
+  let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
   Tacticals.New.tclTHENLASTn
     (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id]))
     (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l)
@@ -2372,8 +2370,8 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     Tacticals.New.tclTHENFIRST eqtac (tac thin)
   end }
 
-let prepare_naming loc = function
-  | IntroIdentifier id -> NamingMustBe (loc,id)
+let prepare_naming ?loc = function
+  | IntroIdentifier id -> NamingMustBe (Loc.tag ?loc id)
   | IntroAnonymous -> NamingAvoid []
   | IntroFresh id -> NamingBasedOn (id,[])
 
@@ -2415,7 +2413,7 @@ let make_tmp_naming avoid l = function
      case of IntroFresh, we should use check_thin_clash_then anyway to
      prevent the case of an IntroFresh precisely using the wild_id *)
   | IntroWildcard -> NamingBasedOn (wild_id,avoid@explicit_intro_names l)
-  | pat -> NamingAvoid(avoid@explicit_intro_names ((dloc,IntroAction pat)::l))
+  | pat -> NamingAvoid(avoid@explicit_intro_names ((Loc.tag @@ IntroAction pat)::l))
 
 let fit_bound n = function
   | None -> true
@@ -2451,7 +2449,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
   | [] ->
       (* Behave as IntroAnonymous *)
       intro_patterns_core with_evars b avoid ids thin destopt bound n tac
-        [dloc,IntroNaming IntroAnonymous]
+        [Loc.tag @@ IntroNaming IntroAnonymous]
   | (loc,pat) :: l ->
   if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else
   match pat with
@@ -2463,7 +2461,7 @@ let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac =
   | IntroAction pat ->
       intro_then_gen (make_tmp_naming avoid l pat)
 	destopt true false
-        (intro_pattern_action loc with_evars (b || not (List.is_empty l)) false
+        (intro_pattern_action ~loc with_evars (b || not (List.is_empty l)) false
           pat thin destopt
           (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0
             (fun ids thin ->
@@ -2488,21 +2486,21 @@ and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac
 	destopt true false
         (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)
 
-and intro_pattern_action loc with_evars b style pat thin destopt tac id =
+and intro_pattern_action ?loc with_evars b style pat thin destopt tac id =
   match pat with
   | IntroWildcard ->
-      tac ((loc,id)::thin) None []
+      tac ((Loc.tag ?loc id)::thin) None []
   | IntroOrAndPattern ll ->
-      intro_or_and_pattern loc with_evars b ll thin tac id
+      intro_or_and_pattern ?loc with_evars b ll thin tac id
   | IntroInjection l' ->
-      intro_decomp_eq loc l' thin tac id
+      intro_decomp_eq ?loc l' thin tac id
   | IntroRewrite l2r ->
       rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None [])
   | IntroApplyOn ((loc',f),(loc,pat)) ->
       let naming,tac_ipat =
-        prepare_intros_loc loc with_evars (IntroIdentifier id) destopt pat in
+        prepare_intros ~loc with_evars (IntroIdentifier id) destopt pat in
       let doclear =
-        if naming = NamingMustBe (loc,id) then
+        if naming = NamingMustBe (Loc.tag ~loc id) then
           Proofview.tclUNIT () (* apply_in_once do a replacement *)
         else
           clear [id] in
@@ -2513,18 +2511,18 @@ and intro_pattern_action loc with_evars b style pat thin destopt tac id =
       apply_in_delayed_once false true true with_evars naming id (None,(loc',f))
         (fun id -> Tacticals.New.tclTHENLIST [doclear; tac_ipat id; tac thin None []])
 
-and prepare_intros_loc loc with_evars dft destopt = function
+and prepare_intros ?loc with_evars dft destopt = function
   | IntroNaming ipat ->
-      prepare_naming loc ipat,
+      prepare_naming ?loc ipat,
       (fun id -> move_hyp id destopt)
   | IntroAction ipat ->
-      prepare_naming loc dft,
+      prepare_naming ?loc dft,
       (let tac thin bound =
         intro_patterns_core with_evars true [] [] thin destopt bound 0
           (fun _ l -> clear_wildcards l) in
       fun id ->
-        intro_pattern_action loc with_evars true true ipat [] destopt tac id)
-  | IntroForthcoming _ -> user_err ~loc 
+        intro_pattern_action ?loc with_evars true true ipat [] destopt tac id)
+  | IntroForthcoming _ -> user_err ?loc 
       (str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to with_evars n destopt =
@@ -2536,7 +2534,7 @@ let intro_patterns_to with_evars destopt =
     [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
 
 let intro_pattern_to with_evars destopt pat =
-  intro_patterns_to with_evars destopt [dloc,pat]
+  intro_patterns_to with_evars destopt [Loc.tag pat]
 
 let intro_patterns with_evars = intro_patterns_to with_evars MoveLast
 
@@ -2549,20 +2547,20 @@ let intros_patterns with_evars = function
 (*   Forward reasoning    *)
 (**************************)
 
-let prepare_intros with_evars dft destopt = function
-  | None -> prepare_naming dloc dft, (fun _id -> Proofview.tclUNIT ())
-  | Some (loc,ipat) -> prepare_intros_loc loc with_evars dft destopt ipat
+let prepare_intros_opt with_evars dft destopt = function
+  | None -> prepare_naming dft, (fun _id -> Proofview.tclUNIT ())
+  | Some (loc,ipat) -> prepare_intros ~loc with_evars dft destopt ipat
 
 let ipat_of_name = function
   | Anonymous -> None
-  | Name id -> Some (dloc, IntroNaming (IntroIdentifier id))
+  | Name id -> Some (Loc.tag @@ IntroNaming (IntroIdentifier id))
 
 let head_ident sigma c =
    let c = fst (decompose_app sigma (snd (decompose_lam_assum sigma c))) in
    if isVar sigma c then Some (destVar sigma c) else None
 
 let assert_as first hd ipat t =
-  let naming,tac = prepare_intros false IntroAnonymous MoveLast ipat in
+  let naming,tac = prepare_intros_opt false IntroAnonymous MoveLast ipat in
   let repl = do_replace hd naming in
   let tac = if repl then (fun id -> Proofview.tclUNIT ()) else tac in
   if first then assert_before_then_gen repl naming t tac
@@ -2580,10 +2578,10 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     if with_evars then MoveLast (* evars would depend on the whole context *)
     else get_previous_hyp_position id gl in
   let naming,ipat_tac =
-    prepare_intros with_evars (IntroIdentifier id) destopt ipat in
+    prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
   let lemmas_target, last_lemma_target =
     let last,first = List.sep_last lemmas in
-    List.map (fun lem -> (NamingMustBe (dloc,id),lem)) first, (naming,last)
+    List.map (fun lem -> (NamingMustBe (Loc.tag id),lem)) first, (naming,last)
   in
   (* We chain apply_in_once, ending with an intro pattern *)
   List.fold_right tac lemmas_target (tac last_lemma_target ipat_tac) id
@@ -2661,7 +2659,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
     let tac =
       Tacticals.New.tclTHENLIST
       [ convert_concl_no_check newcl DEFAULTcast;
-        intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false;
+        intro_gen (NamingMustBe (Loc.tag id)) (decode_hyp lastlhyp) true false;
         Tacticals.New.tclMAP convert_hyp_no_check depdecls;
         eq_tac ]
     in
@@ -2961,7 +2959,7 @@ let specialize (c,lbind) ipat =
     | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) ->
       (* Like assert (id:=id args) but with the concept of specialization *)
       let naming,tac =
-        prepare_intros false (IntroIdentifier id) MoveLast ipat in
+        prepare_intros_opt false (IntroIdentifier id) MoveLast ipat in
       let repl = do_replace (Some id) naming in
       Tacticals.New.tclTHENFIRST
         (assert_before_then_gen repl naming typ tac)
@@ -2975,7 +2973,7 @@ let specialize (c,lbind) ipat =
       | Some (loc,ipat) ->
         (* Like pose proof with extra support for "with" bindings *)
         (* even though the "with" bindings forces full application *)
-        let naming,tac = prepare_intros_loc loc false IntroAnonymous MoveLast ipat in
+        let naming,tac = prepare_intros ~loc false IntroAnonymous MoveLast ipat in
         Tacticals.New.tclTHENFIRST
           (assert_before_then_gen false naming typ tac)
 	  (exact_no_check term)
@@ -3063,7 +3061,7 @@ let intropattern_of_name gl avoid = function
   | Name id -> IntroNaming (IntroIdentifier (new_fresh_id avoid id gl))
 
 let rec consume_pattern avoid na isdep gl = function
-  | [] -> ((dloc, intropattern_of_name gl avoid na), [])
+  | [] -> ((Loc.tag @@ intropattern_of_name gl avoid na), [])
   | (loc,IntroForthcoming true)::names when not isdep ->
       consume_pattern avoid na isdep gl names
   | (loc,IntroForthcoming _)::names as fullpat ->
@@ -3140,7 +3138,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
         let (recpat,names) = match names with
           | [loc,IntroNaming (IntroIdentifier id) as pat] ->
               let id' = next_ident_away (add_prefix "IH" id) avoid in
-	      (pat, [dloc, IntroNaming (IntroIdentifier id')])
+	      (pat, [Loc.tag @@ IntroNaming (IntroIdentifier id')])
           | _ -> consume_pattern avoid (Name recvarname) deprec gl names in
         let dest = get_recarg_dest dests in
         dest_intro_patterns with_evars avoid thin dest [recpat] (fun ids thin ->
@@ -5026,14 +5024,14 @@ module Simple = struct
   let intro x = intro_move (Some x) MoveLast
 
   let apply c =
-    apply_with_bindings_gen false false [None,(Loc.ghost,(c,NoBindings))]
+    apply_with_bindings_gen false false [None,(Loc.tag (c,NoBindings))]
   let eapply c =
-    apply_with_bindings_gen false true [None,(Loc.ghost,(c,NoBindings))]
+    apply_with_bindings_gen false true [None,(Loc.tag (c,NoBindings))]
   let elim c   = elim false None (c,NoBindings) None
   let case   c = general_case_analysis false None (c,NoBindings)
 
   let apply_in id c =
-    apply_in false false id [None,(Loc.ghost, (c, NoBindings))] None
+    apply_in false false id [None,(Loc.tag (c, NoBindings))] None
 
 end