[location] More located use.

4 files changed, 8 insertions, 8 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4f23dd2ab5..61115c00b5 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 bbc98dd28e..8d9f8552dc 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 cc7203ac00..d1b931a227 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 c3e341d74f..c8fbdaf285 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)