From a60a49f545499f29f067148668b8ec1bc7b55895 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 14 Dec 2017 11:39:24 -0500 Subject: Pass a ghost location for abstract As per request at https://github.com/coq/coq/pull/6406#pullrequestreview-83503902 --- plugins/ltac/g_ltac.ml4 | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/ltac/g_ltac.ml4') diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8dd4199e3..ebf6e450b 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -125,9 +125,9 @@ GEXTEND Gram | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta (*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (Loc.tag ~loc:!@loc (tc,None)) + | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (Loc.tag ~loc:!@loc (tc,Some s)) + TacAbstract (tc,Some s) | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] (*End of To do*) | "2" RIGHTA @@ -401,12 +401,12 @@ VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default END let is_anonymous_abstract = function - | TacAbstract (_,(_,None)) -> true - | TacSolve [TacAbstract (_,(_,None))] -> true + | TacAbstract (_,None) -> true + | TacSolve [TacAbstract (_,None)] -> true | _ -> false let rm_abstract = function - | TacAbstract (_,(t,_)) -> t - | TacSolve [TacAbstract (_,(t,_))] -> TacSolve [t] + | TacAbstract (t,_) -> t + | TacSolve [TacAbstract (t,_)] -> TacSolve [t] | x -> x let is_explicit_terminator = function TacSolve _ -> true | _ -> false -- cgit v1.2.3