From 6b45f2d36929162cf92272bb60c2c245d9a0ead3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 22 Jun 2012 15:14:30 +0000
Subject: Added an indirection with respect to Loc in Compat. As many [open
 Compat] were closed (i.e. the only remaining ones are those of
 printing/parsing). Meanwhile, a simplified interface is provided in loc.mli.

This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extraargs.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics/extraargs.ml4')

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index bff4f47601..7bfda9802c 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -125,7 +125,7 @@ END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = identifier Pp.located gen_place
+type loc_place = identifier Loc.located gen_place
 type place = identifier gen_place
 
 let pr_gen_place pr_id = function
@@ -167,11 +167,11 @@ ARGUMENT EXTEND hloc
   |  [ "in" "|-" "*" ] ->
     [ ConclLocation () ]
 | [ "in" ident(id) ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHyp) ]
+    [ HypLocation ((Loc.ghost,id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHypTypeOnly) ]
+    [ HypLocation ((Loc.ghost,id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
-    [ HypLocation ((Pp.dummy_loc,id),InHypValueOnly) ]
+    [ HypLocation ((Loc.ghost,id),InHypValueOnly) ]
 
  END
 
-- 
cgit v1.2.3