diff options
| author | herbelin | 2004-07-16 16:05:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-07-16 16:05:56 +0000 |
| commit | 5542b28bc21866daf10634120cbd731c2092bd92 (patch) | |
| tree | ab7dabdb3cf2e5bb1319b5e614d0027483bfa1b1 | |
| parent | 2429e5b881d0b3719c4e5bbc023cb94f9a3f80bc (diff) | |
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
| -rw-r--r-- | parsing/tacextend.ml4 | 7 | ||||
| -rw-r--r-- | 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 |