From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 474cc85c17..52cf8cf97d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -26,7 +26,7 @@ open Clenv
 let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
+let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
 
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
-- 
cgit v1.2.3