From 84eb5cd72a015c45337a5a6070c5651f56be6e74 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 17 Jan 2017 15:45:43 +0100
Subject: [location] Use located in tactics.

One case missing due the TACTIC EXTEND macro.
---
 plugins/ltac/g_ltac.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/g_ltac.ml4')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index dffd90be3..d6cbd8db1 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -161,7 +161,7 @@ GEXTEND Gram
       | st = simple_tactic -> st
       | a = tactic_arg -> TacArg(!@loc,a)
       | r = reference; la = LIST0 tactic_arg_compat ->
-          TacArg(!@loc,TacCall (!@loc,r,la)) ]
+          TacArg(!@loc, TacCall (!@loc,(r,la))) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
       | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
@@ -219,7 +219,7 @@ GEXTEND Gram
   ;
   tactic_atom:
     [ [ n = integer -> TacGeneric (genarg_of_int n)
-      | r = reference -> TacCall (!@loc,r,[])
+      | r = reference -> TacCall (!@loc,(r,[]))
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
   match_key:
-- 
cgit v1.2.3