[location] Use Loc.located for constr_expr.

This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.

Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.

6 files changed, 24 insertions, 24 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c2..dffd90be3 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -187,7 +187,7 @@ GEXTEND Gram
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
     [ [ a = tactic_arg -> a
-      | c = Constr.constr -> (match c with CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
+      | c = Constr.constr -> (match c with _loc, CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
       (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
@@ -255,10 +255,10 @@ GEXTEND Gram
 	  let t, ty =
 	    match mpv with
 	    | Term t -> (match t with
-	      | CCast (loc, t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
+	      | _loc, CCast (t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (CHole (Loc.ghost, None, IntroAnonymous, None))) ty)
+	  in Def (na, t, Option.default (Term (Loc.tag @@ CHole (None, IntroAnonymous, None))) ty)
     ] ]
   ;
   match_context_rule:
@@ -353,7 +353,7 @@ GEXTEND Gram
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
-          CHole (!@loc, None, IntroAnonymous, Some arg) ] ]
+          Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
   ;
   END
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 4b3ca80af..1674bb4ca 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -130,14 +130,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
           (try List.index Names.Name.equal (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
-  (id,n,CProdN(loc,bl,ty))
+  (id,n, Loc.tag ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     user_err ~loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
-  (id,CProdN(loc,bl,ty))
+  (id,Loc.tag ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
@@ -154,12 +154,12 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)),
+        (clear,(Loc.tag @@ CPrim (Numeral (Bigint.of_int n)),
 	 NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-      TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings)))
+      TacCase (with_evar,(clear,(Loc.tag @@ CRef (Ident id,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
@@ -169,7 +169,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CLambdaN (loc,[idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
+      Loc.tag ~loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc (Loc.merge loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc loc bll c
   | [] -> c
 
@@ -440,7 +440,7 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit,CHole (!@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+    [ [ na=name -> ([na],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 39ae1f41d..ad76ef9c6 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -340,8 +340,8 @@ type 'a extra_genarg_printer =
 
   let strip_prod_binders_expr n ty =
     let rec strip_ty acc n ty =
-      match ty with
-          Constrexpr.CProdN(_,bll,a) ->
+      match snd ty with
+          Constrexpr.CProdN(bll,a) ->
             let nb =
               List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
             let bll = List.map (fun (x, _, y) -> x, y) bll in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600..1f75f88d4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1787,18 +1787,18 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
+let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.ghost,Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
   (((Loc.ghost,Name n),None), Explicit,
-  CAppExpl (Loc.ghost, (None, Qualid (Loc.ghost, qualid_of_string s),None),
+  Loc.tag @@ CAppExpl ((None, Qualid (Loc.ghost, qualid_of_string s),None),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
-    binders instance (Some (true, CRecord (Loc.ghost,fields)))
+    binders instance (Some (true, Loc.tag @@ CRecord (fields)))
     ~global ~generalize:false ~refine:false Hints.empty_hint_info
 
 let declare_instance_refl global binders a aeq n lemma =
@@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None)
+let cHole = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None)
 
 let proper_projection sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
@@ -2013,13 +2013,13 @@ let add_morphism glob binders m s n =
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((Loc.ghost,Name instance_id),None), Explicit,
-    CAppExpl (Loc.ghost,
+    Loc.tag @@ CAppExpl (
 	     (None, Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
     ignore(new_instance ~global:glob poly binders instance 
-	     (Some (true, CRecord (Loc.ghost,[])))
+	     (Some (true, Loc.tag @@ CRecord []))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 3f83f104e..75f890c96 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -110,13 +110,13 @@ 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 (CRef (r,None))
+      GVar (dloc,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 (CRef (r,None))
+      GVar (dloc,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), 
-	if strict then None else Some (CRef (r,None))
+	if strict then None else Some (Loc.tag @@ CRef (r,None))
 
 let intern_move_location ist = function
   | MoveAfter id -> MoveAfter (intern_hyp ist id)
@@ -273,7 +273,7 @@ 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 (CRef (Ident (dloc,id), None)) with
+	match intern_constr ist (Loc.tag @@ CRef (Ident (dloc,id), None)) with
 	| GVar (loc,id),_ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
@@ -363,7 +363,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
-  | Inr (CAppExpl(_,(None,r,None),[])) ->
+  | Inr (_, CAppExpl((None,r,None),[])) ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 50f43931e..de6c44b2b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -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 (CRef (Ident (loc,id),None))) in
+          let c = (GVar (loc,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