From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Jan 2017 23:40:35 +0100 Subject: [location] Remove Loc.ghost. Now it is a private field, locations are optional. --- vernac/indschemes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/indschemes.ml') diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9ba4e46e4..2367177e2 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -379,7 +379,7 @@ requested | InType -> recs ^ "t_nodep") ) in let newid = add_suffix (basename_of_global (IndRef ind)) suffix in - let newref = (Loc.ghost,newid) in + let newref = Loc.tag newid in ((newref,isdep,ind,z)::l1),l2 in match t with -- cgit v1.2.3