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

---
 vernac/command.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'vernac/command.ml')

diff --git a/vernac/command.ml b/vernac/command.ml
index 1f14648561..446afb5787 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -422,13 +422,13 @@ let prepare_param = function
     
 let rec check_anonymous_type ind =
   let open Glob_term in
-    match ind with
-    | GSort (_, GType []) -> true
-    | GProd (_, _, _, _, e) 
-    | GLetIn (_, _, _, _, e)
-    | GLambda (_, _, _, _, e)
-    | GApp (_, e, _)
-    | GCast (_, e, _) -> check_anonymous_type e
+    match snd ind with
+    | GSort (GType []) -> true
+    | GProd ( _, _, _, e) 
+    | GLetIn (_, _, _, e)
+    | GLambda (_, _, _, e)
+    | GApp (e, _)
+    | GCast (e, _) -> check_anonymous_type e
     | _ -> false
 
 let make_conclusion_flexible evdref ty poly =
-- 
cgit v1.2.3