[location] More located use.

8 files changed, 17 insertions, 17 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4f23dd2ab..61115c00b 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -239,7 +239,7 @@ let local_binder_loc = function
   | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
   | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t))
   | CLocalAssum ([],_,_) -> assert false
-  | CLocalPattern (loc,_,_) -> loc
+  | CLocalPattern (loc,_) -> loc
 
 let local_binders_loc bll = match bll with
   | [] -> Loc.ghost
@@ -283,7 +283,7 @@ let expand_binders ~loc mkC bl c =
             let env = List.fold_left add_name_in_env env nl in
             (env, mkC ~loc (nl,bk,t) c)
         | CLocalAssum ([],_,_) -> loop loc bl c
-        | CLocalPattern (loc1, p, ty) ->
+        | CLocalPattern (loc1, (p, ty)) ->
             let env, c = loop ~loc:(Loc.merge loc1 loc) bl c in
             let ni = Hook.get fresh_var env c in
             let id = (loc1, Name ni) in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bbc98dd28..8d9f8552d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -866,7 +866,7 @@ and extern_local_binder scopes vars = function
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = extern_cases_pattern vars p in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
+      (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
 
 and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
   Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cc7203ac0..d1b931a22 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -475,7 +475,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
      let ty = Option.map (intern env) ty in
       (push_name_env lvar (impls_term_list term) env locna,
        GLocalDef (loc,na,Explicit,term,ty) :: bl)
-  | CLocalPattern (loc,p,ty) ->
+  | CLocalPattern (loc,(p,ty)) ->
       let tyc =
         match ty with
         | Some ty -> ty
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c3e341d74..c8fbdaf28 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -97,7 +97,7 @@ let rec fold_local_binders g f n acc b = function
       f n (fold_local_binders g f n' acc b l) t
   | CLocalDef ((_,na),c,t)::l ->
       Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
-  | CLocalPattern (_,pat,t)::l ->
+  | CLocalPattern (_,(pat,t))::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
   | [] ->
@@ -180,7 +180,7 @@ let split_at_annot bl na =
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
 	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
-        | CLocalPattern (loc,_,_) :: rest ->
+        | CLocalPattern (loc,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ~loc 
@@ -204,9 +204,9 @@ let map_local_binders f g e bl =
         (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
     | CLocalDef((loc,na),c,ty) ->
         (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
-    | CLocalPattern (loc,pat,t) ->
+    | CLocalPattern (loc,(pat,t)) ->
         let ids = ids_of_pattern pat in
-        (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in
+        (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index c1ea71df4..92d0020a5 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -125,9 +125,9 @@ and recursion_order_expr =
 
 (** Anonymous defs allowed ?? *)
 and local_binder_expr =
-  | CLocalAssum of Name.t located list * binder_kind * constr_expr
-  | CLocalDef of Name.t located * constr_expr * constr_expr option
-  | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option
+  | CLocalAssum   of Name.t located list * binder_kind * constr_expr
+  | CLocalDef     of Name.t located * constr_expr * constr_expr option
+  | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9bf00b0b1..33e7236f5 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -486,7 +486,7 @@ GEXTEND Gram
             | _, CPatCast (p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
-          [CLocalPattern (!@loc, p, ty)]
+          [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))]
     ] ]
   ;
   typeclass_constraint:
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index a99c0951f..117e1900d 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -319,7 +319,7 @@ let tag_var = tag Tag.variable
   let begin_of_binder = function
     | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc)
     | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
-    | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc)
+    | CLocalPattern(loc,(_,_)) -> fst (Loc.unloc loc)
     | _ -> assert false
 
   let begin_of_binders = function
@@ -366,7 +366,7 @@ let tag_var = tag Tag.variable
       surround (pr_lname na ++
                 pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++
                 str" :=" ++ spc() ++ pr_c c)
-    | CLocalPattern (loc,p,tyo) ->
+    | CLocalPattern (loc,(p,tyo)) ->
       let p = pr_patt lsimplepatt p in
       match tyo with
         | None ->
@@ -400,7 +400,7 @@ let tag_var = tag Tag.variable
               (_loc', CCases (LetPatternStyle,None, [(_loc'', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))])))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
-      CLocalPattern (loc, p,None) :: bl, c
+      CLocalPattern (loc, (p,None)) :: bl, c
     | loc, CProdN ((nal,bk,t)::bl,c) ->
       let bl,c = extract_prod_binders (loc, CProdN(bl,c)) in
       CLocalAssum (nal,bk,t) :: bl, c
@@ -416,7 +416,7 @@ let tag_var = tag Tag.variable
                 (_loc, CCases (LetPatternStyle,None, [(_loc', CRef (Ident (_,id'),None)),None,None],[(_,([_,[p]],b))])))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
-      CLocalPattern (loc,p,None) :: bl, c
+      CLocalPattern (loc,(p,None)) :: bl, c
     | CLambdaN ((nal,bk,t)::bl,c) ->
       let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in
       CLocalAssum (nal,bk,t) :: bl, c
diff --git a/vernac/record.ml b/vernac/record.ml
index 37ce231f9..95f5ad7cc 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -112,7 +112,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       List.iter 
 	(function CLocalDef (b, _, _) -> error default_binder_kind b
 	   | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | CLocalPattern (loc,_,_) ->
+           | CLocalPattern (loc,(_,_)) ->
               Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in