aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/tacexpr.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index eefee41f5f..b63588aaa4 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -209,7 +209,8 @@ and ('constr,'cst,'ind,'id) gen_tactic_arg =
| ConstrMayEval of 'constr may_eval
| Reference of reference_expr
| Integer of int
- | TacCall of loc * ('constr,'cst,'ind,'id) gen_tactic_arg * ('constr,'cst,'ind,'id) gen_tactic_arg list
+ | TacCall of loc *
+ reference_expr * ('constr,'cst,'ind,'id) gen_tactic_arg list
| Tacexp of raw_tactic_expr
type raw_atomic_tactic_expr =