From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 16 Jan 2017 13:02:55 +0100
Subject: [location] Move Glob_term.cases_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 pretyping/coercion.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdf..b2c1d0116 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -78,8 +78,9 @@ let apply_coercion_args env evd check isproj argl funj =
 let apply_pattern_coercion loc pat p =
   List.fold_left
     (fun pat (co,n) ->
-       let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
-	 Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous))
+       let f i =
+         if i<n then (Loc.tag ~loc @@ Glob_term.PatVar Anonymous) else pat in
+        Loc.tag ~loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
     pat p
 
 (* raise Not_found if no coercion found *)
-- 
cgit v1.2.3