aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacsubst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacsubst.ml')
-rw-r--r--plugins/ltac/tacsubst.ml2
1 files changed, 1 insertions, 1 deletions
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