diff options
Diffstat (limited to 'parsing/tacextend.ml4')
| -rw-r--r-- | parsing/tacextend.ml4 | 7 |
1 files changed, 4 insertions, 3 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$ |