[location] Switch glob_constr to Loc.located

5 files changed, 21 insertions, 23 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 38fdfb7599..232bd851ff 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -631,15 +631,15 @@ let subst_var_with_hole occ tid t =
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
   let rec substrec = function
-    | GVar (_,id) as x -> 
+    | (_, GVar id) as x -> 
         if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
            else
 	     (incr locref;
-	      GHole (Loc.make_loc (!locref,0),
-		     Evar_kinds.QuestionMark(Evar_kinds.Define true),
+              Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
                      Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -651,13 +651,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
+    | _, GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
-	   GHole (Loc.make_loc (!locref,0),
-		  Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+           Loc.tag ~loc:(Loc.make_loc (!locref,0)) @@
+	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf55..1f40c67b5d 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
+  let is_tac id = match fst (fst (snd c)) with (_, GVar id') when Id.equal id' id -> true | _ -> false in
     Tacticals.onAllHypsAndConcl
       (fun cl ->
         match cl with
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index ad76ef9c65..aec2e37fde 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1085,8 +1085,8 @@ type 'a extra_genarg_printer =
   let strip_prod_binders_glob_constr n (ty,_) =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
-        match ty with
-            Glob_term.GProd(loc,na,Explicit,a,b) ->
+        match Loc.obj ty with
+            Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.ghost,na],(a,None))::acc) (n-1) b
           | _ -> error "Cannot translate fix tactic: not enough products" in
     strip_ty [] n ty
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 75f890c960..e7d4c1be9f 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -31,8 +31,6 @@ open Locus
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
-let dloc = Loc.ghost
-
 let error_tactic_expected ?loc =
   user_err ?loc  (str "Tactic expected.")
 
@@ -74,14 +72,14 @@ let intern_name l ist = function
 
 let strict_check = ref false
 
-let adjust_loc loc = if !strict_check then dloc else loc
+let adjust_loc loc = if !strict_check then Loc.ghost else loc
 
 (* Globalize a name which must be bound -- actually just check it is bound *)
 let intern_hyp ist (loc,id as locid) =
   if not !strict_check then
     locid
   else if find_ident id ist then
-    (dloc,id)
+    Loc.tag id
   else
     Pretype_errors.error_var_not_found ~loc id
 
@@ -110,12 +108,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      GVar (dloc,id), Some (Loc.tag @@ CRef (r,None))
+      (Loc.tag @@ GVar id), Some (Loc.tag @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      GVar (dloc,id), if strict then None else Some (Loc.tag @@ CRef (r,None))
+      (Loc.tag @@ GVar id), if strict then None else Some (Loc.tag @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      GRef (loc,locate_global_with_alias lqid,None), 
+      Loc.tag @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (Loc.tag @@ CRef (r,None))
 
 let intern_move_location ist = function
@@ -273,8 +271,8 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	match intern_constr ist (Loc.tag @@ CRef (Ident (dloc,id), None)) with
-	| GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
+	match intern_constr ist (Loc.tag @@ CRef (Ident (Loc.tag id), None)) with
+	| (loc, GVar id), _ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
 	clear,ElimOnIdent (loc,id)
@@ -352,10 +350,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       | _ -> Qualid (loc,qualid_of_path (path_of_global (smart_global r))) in
       let sign = { Constrintern.ltac_vars = ist.ltacvars; Constrintern.ltac_bound = Id.Set.empty } in
       let c = Constrintern.interp_reference sign r in
-      match c with
-      | GRef (_,r,None) ->
+      match Loc.obj c with
+      | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
-      | GVar (_,id) ->
+      | GVar id ->
           let r = evaluable_of_global_reference ist.genv (VarRef id) in
           Inl (ArgArg (r,None))
       | _ ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index de6c44b2b9..a8d8eda1dd 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -699,7 +699,7 @@ let interp_typed_pattern ist env sigma (_,c,_) =
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
     try match dest_fun x with
-    | GVar (_,id), _ ->
+    | (_, GVar id), _ ->
       let v = Id.Map.find id ist.lfun in
       sigma, List.map inj_fun (coerce_to_constr_list env v)
     | _ ->
@@ -1074,7 +1074,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (GVar (loc,id),Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
+          let c = (Loc.tag ~loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in