diff options
| -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 |