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

---
 plugins/setoid_ring/newring.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index dd68eac24c..bef8139bef 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -131,7 +131,7 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.ghost,tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None));
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (Loc.tag @@ GVar(Id.of_string"t"),None));
    TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
-- 
cgit v1.2.3