From 5542b28bc21866daf10634120cbd731c2092bd92 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Jul 2004 16:05:56 +0000
Subject: Abstraction vis a vis de dummy_loc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5910 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/tacextend.ml4    | 7 ++++---
 parsing/vernacextend.ml4 | 4 ++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 2b3c17b149..85ea38677f 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -14,8 +14,8 @@ open Q_coqast
 open Argextend
 
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
-let loc = (0,0)
-let default_loc = <:expr< (0,0) >>
+let loc = Util.dummy_loc
+let default_loc = <:expr< Util.dummy_loc >>
 
 type grammar_tactic_production_expr =
   | TacTerm of string
@@ -204,7 +204,8 @@ let declare_tactic loc s cl =
         let _=Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) in
         List.iter
           (fun s -> Tacinterp.add_primitive_tactic s
-              (Tacexpr.TacAtom((0,0),Tacexpr.TacExtend((0,0),s,[]))))
+              (Tacexpr.TacAtom($default_loc$,
+                 Tacexpr.TacExtend($default_loc$,s,[]))))
           $atomic_tactics$
       with e -> Pp.pp (Cerrors.explain_exn e);
       if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 127b411b5d..07ad238297 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -15,8 +15,8 @@ open Ast
 open Argextend
 
 let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
-let loc = (0,0)
-let default_loc = <:expr< (0,0) >>
+let loc = Util.dummy_loc
+let default_loc = <:expr< Util.dummy_loc >>
 
 type grammar_tactic_production_expr =
   | VernacTerm of string
-- 
cgit v1.2.3