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
---
 plugins/firstorder/g_ground.ml4 | 2 +-
 plugins/firstorder/instances.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b009107dce..3f0c704ad9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -107,7 +107,7 @@ open Genarg
 open Ppconstr
 open Printer
 let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference
-let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_located pr_global))
+let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global))
 let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
 
 ARGUMENT EXTEND firstorder_using
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index bc15cb5015..195e6afa3f 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -128,7 +128,7 @@ let mk_open_instance id gl m t=
       match t with
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      GLambda(loc,name,k,GHole (dummy_loc,Evar_kinds.BinderType name),t1)
+	      GLambda(loc,name,k,GHole (Loc.ghost,Evar_kinds.BinderType name),t1)
 	| _-> anomaly "can't happen" in
   let ntt=try
     Pretyping.understand evmap env (raux m rawt)
-- 
cgit v1.2.3