From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [location] Make location optional in Loc.located This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed and other times it printed nothing as the caller checked for `is_ghost` upstream. --- plugins/ltac/tacsubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac/tacsubst.ml') diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 0ee6e8a85..4390ff08b 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -242,7 +242,7 @@ and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) | TacCall (loc,(f,l)) -> - TacCall (Loc.tag ~loc (subst_reference subst f, List.map (subst_tacarg subst) l)) + TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l)) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals -- cgit v1.2.3