[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.

4 files changed, 20 insertions, 18 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 833719965..ffe03bfb7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -147,14 +147,14 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	  (fun avoid (clname, _) ->
 	    match clname with
 	    | Some (cl, b) ->
-		let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
+		let t = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
     | Explicit -> cl, Id.Set.empty
   in
   let tclass = 
-    if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) 
+    if generalize then Loc.tag @@ CGeneralization (Implicit, Some AbsPi, tclass) 
     else tclass 
   in
   let k, u, cty, ctx', ctx, len, imps, subst =
@@ -217,7 +217,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
     else (
       let props =
 	match props with
-	| Some (true, CRecord (loc, fs)) ->
+	| Some (true, (_loc, CRecord fs)) ->
 	    if List.length fs > List.length k.cl_props then
 	      mismatched_props env' (List.map snd fs) k.cl_props;
 	    Some (Inl fs)
@@ -261,7 +261,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Loc.ghost, None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None) :: props), rest
+		       ((Loc.tag @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
diff --git a/vernac/command.ml b/vernac/command.ml
index 45ff57955..1f1464856 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -53,18 +53,19 @@ let rec under_binders env sigma f n c =
 	  mkLetIn (x,b,t,under_binders (push_rel (LocalDef (x,b,t)) env) sigma f (n-1) c)
       | _ -> assert false
 
-let rec complete_conclusion a cs = function
-  | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
-  | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c)
-  | CHole (loc, k, _, _) ->
+let rec complete_conclusion a cs = Loc.map_with_loc (fun ~loc -> function
+  | CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
+  | CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
+  | CHole (k, _, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
-	user_err ~loc 
+	user_err ~loc
 	 (strbrk"Cannot infer the non constant arguments of the conclusion of "
 	  ++ pr_id cs ++ str ".");
-      let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
-      CAppExpl (loc,(None,Ident(loc,name),None),List.rev args)
+      let args = List.map (fun id -> Loc.tag ~loc @@ CRef(Ident(loc,id),None)) params in
+      CAppExpl ((None,Ident(loc,name),None),List.rev args)
   | c -> c
+  )
 
 (* Commands of the interface *)
 
@@ -682,7 +683,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun (((_,indname),pl),_,ar,lc) -> {
     ind_name = indname; ind_univs = pl;
-    ind_arity = Option.cata (fun x -> x) (CSort (Loc.ghost,GType [])) ar;
+    ind_arity = Option.cata (fun x -> x) (Loc.tag @@ CSort (GType [])) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
@@ -1354,7 +1355,7 @@ let do_program_fixpoint local poly l =
 	     
     | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
 	build_wellfounded (id, pl, n, bl, typ, out_def def) poly
-	  (Option.default (CRef (lt_ref,None)) r) m ntn
+	  (Option.default (Loc.tag @@ CRef (lt_ref,None)) r) m ntn
 	  
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
 	let fixl,ntns = extract_fixpoint_components true l in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f805eeaa9..98b2c3729 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v =
 
 (* Infix notations *)
 
-let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None)
+let inject_var x = Loc.tag @@ CRef (Ident (Loc.ghost, Id.of_string x),None)
 
 let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
@@ -1477,7 +1477,7 @@ let add_class_scope scope cl =
 (* Check if abbreviation to a name and avoid early insertion of
    maximal implicit arguments *)
 let try_interp_name_alias = function
-  | [], CRef (ref,_) -> intern_reference ref
+  | [], (_loc, CRef (ref,_)) -> intern_reference ref
   | _ -> raise Not_found
 
 let add_syntactic_definition ident (vars,c) local onlyparse =
diff --git a/vernac/record.ml b/vernac/record.ml
index 8b4b7606f..37ce231f9 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -93,7 +93,8 @@ let compute_constructor_level evars env l =
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
-  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None, Misctypes.IntroAnonymous, None))
+  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c
+                                                       | None   -> Loc.tag ~loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None))
 
 let binders_of_decls = List.map binder_of_decl
 
@@ -120,8 +121,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     | Some t -> 
        let env = push_rel_context newps env0 in
        let poly =
-         match t with
-         | CSort (_, Misctypes.GType []) -> true | _ -> false in
+         match snd t with
+         | CSort (Misctypes.GType []) -> true | _ -> false in
        let s = interp_type_evars env evars ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_all env !evars s in
        let s = EConstr.Unsafe.to_constr s in