From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 15:06:26 +0100
Subject: [location] Use located in misctypes.

---
 intf/genredexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf/genredexpr.mli')

diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 16f0c0c92a..2a542e0ff2 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of (Loc.t * Id.t) * 'a
+  | ConstrContext of Id.t Loc.located * 'a
   | ConstrTypeOf of 'a
 
 open Libnames
-- 
cgit v1.2.3