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.
---
 plugins/ltac/coretactics.ml4 | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac/coretactics.ml4')

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df838..6890b31981 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -305,10 +305,9 @@ END
 open Tacexpr
 
 let initial_atomic () =
-  let dloc = Loc.ghost in
   let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
   let iter (s, t) =
-    let body = TacAtom (dloc, t) in
+    let body = TacAtom (Loc.tag t) in
     Tacenv.register_ltac false false (Id.of_string s) body
   in
   let () = List.iter iter
@@ -323,7 +322,7 @@ let initial_atomic () =
   List.iter iter
       [ "idtac",TacId [];
         "fail", TacFail(TacLocal,ArgArg 0,[]);
-        "fresh", TacArg(dloc,TacFreshId [])
+        "fresh", TacArg(Loc.tag @@ TacFreshId [])
       ]
 
 let () = Mltop.declare_cache_obj initial_atomic "coretactics"
-- 
cgit v1.2.3